Quelle  integral_convergence_scaf.pvs

%------------------------------------------------------------------------------
% A primitive version of the Monotone Convergence Theorem
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

integral_convergence_scaf[T:TYPE,        (IMPORTING subset_algebra_def[T])
                          S:sigma_algebra,(IMPORTING measure_def[T,S])
                          m:measure_type]: THEORY

BEGIN

  IMPORTING measure_space[T,S],
            measure_theory[T,S,m],
            integral[T,S,m]

  f: VAR [T->real]
  F: VAR sequence[integrable]

  monotone_convergence_scaf: LEMMA                                      % 4.5.1
     pointwise_converges_upto?(F,f) AND bounded?(integral o F) =>
     (integrable?(f) AND converges_upto?((integral o F), integral(f)))

END integral_convergence_scaf