|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
