|
%------------------------------------------------------------------------------
% 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
[ zur Elbe Produktseite wechseln0.2Quellennavigators
Analyse erneut starten
]
|
