| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/C/Goedel/ (Wiener Entwicklungsmethode ©) Datei vom 17.9.2012 mit Größe 4 kB |
|
Quelle complete_measure_theory.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------
% 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.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
