| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/measure_integration/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle product_sigma_def.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Product sigma algebras % % Author: David Lester, Manchester University, NIA, Université Perpignan % % All references are to SK Berberian, "Fundamentals of Real Analysis" % Springer, 1999 % % Version 1.0 11/09/08 Initial Version %------------------------------------------------------------------------------ product_sigma_def[T1,T2:TYPE]: THEORY BEGIN IMPORTING subset_algebra_def, sigma_algebra, topology@cross_product[T1,T2], product_sections[T1,T2], sets_aux@countable_image % Proof Only i,n: VAR nat x: VAR T1 y: VAR T2 X: VAR set[T1] Y: VAR set[T2] NX: VAR (nonempty?[T1]) NY: VAR (nonempty?[T2]) Z: VAR set[[T1,T2]] S1: VAR sigma_algebra[T1] S2: VAR sigma_algebra[T2] measurable_rectangle?(S1,S2)(Z):bool = EXISTS X,Y: Z = cross_product(X,Y) AND S1(X) AND S2(Y) measurable_rectangle(S1,S2): TYPE+ = (measurable_rectangle?(S1,S2)) CONTAINING emptyset sigma_times(S1,S2):sigma_algebra[[T1,T2]] = generated_sigma_algebra(fullset[measurable_rectangle(S1,S2)]) x_section_measurable: LEMMA member(Z,sigma_times(S1,S2)) => member(x_section(Z,x),S2) y_section_measurable: LEMMA member(Z,sigma_times(S1,S2)) => member(y_section(Z,y),S1) sigma_cross_projection: LEMMA % 7.2.7 member(cross_product(NX,NY),sigma_times(S1,S2)) => (member(NX,S1) AND member(NY,S2)) END product_sigma_def ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28