Quelle  finite_integral.pvs   Sprache: unbekannt

%------------------------------------------------------------------------------
% Integrals with finite measure
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% With finite measures (as in probability), every bounded measurable function
% is integrable.
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

finite_integral[T:TYPE,          (IMPORTING subset_algebra_def[T])
                S:sigma_algebra, (IMPORTING measure_def[T,S])
                mu:finite_measure]: THEORY

BEGIN

  IMPORTING integral[T,S,to_measure(mu)]

  bounded_measurable_is_integrable:
     JUDGEMENT bounded_measurable SUBTYPE_OF integrable

END finite_integral