products/sources/formale sprachen/Delphi/Autor 0.7/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Affine.thy   Sprache: Unknown

%------------------------------------------------------------------------------
% 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

[ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ]