Quelle  hahn_kolmogorov.pvs

%------------------------------------------------------------------------------
% Hahn-Kolmogorov Theorem
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Extending a measure from an algebra to a sigma-algebra
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

hahn_kolmogorov[T:TYPE,           (IMPORTING subset_algebra_def[T])
                A:subset_algebra, (IMPORTING measure_def[T,A])
                mu: measure_type]: THEORY

BEGIN

  IMPORTING outer_measure[T,A],
            outer_measure_props[T,ast(mu)]

  x: VAR (A)

  algebra_in_induced_sigma_algebra: LEMMA subset?(A,induced_sigma_algebra)

  IMPORTING measure_theory[T,induced_sigma_algebra,induced_measure]

  induced_measure_measure: LEMMA x_eq(induced_measure(x),mu(x))

END hahn_kolmogorov