|
%-------------------------------------------------------------------------
% Complete Measure Theory
%
% Author: David Lester, Manchester University
%
% Version 1.0 04/05/09 Initial (DRL)
%-------------------------------------------------------------------------
complete_measure_theory[T:TYPE, (IMPORTING subset_algebra_def[T])
S:sigma_algebra, (IMPORTING measure_def[T,S])
mu:complete_measure]: THEORY
BEGIN
IMPORTING measure_space_def[T,S],
sigma_algebra[T,S],
measure_theory[T,S,mu],
measure_props[T,S,mu]
N: VAR null_set
X: VAR set[T]
E: VAR negligible
f: VAR [T->real]
g: VAR measurable_function
null_subset: LEMMA subset?(X,N) => null_set?(X)
null_is_negligible: LEMMA null_set?(X) <=> negligible_set?(X)
ae_eq_measurable: LEMMA ae_eq?(f,g) => measurable_function?(f)
END complete_measure_theory
¤ Dauer der Verarbeitung: 0.15 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.
|
