| 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 |
|
Quellcode-Bibliothek product_sections.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Sections of sets % % Author: David Lester, Manchester University, NIA, Université Perpignan % % All references are to SK Berberian "Fundamentals of Real Analysis", % Springer, 1991 % % Version 1.0 1/5/07 Initial Version %------------------------------------------------------------------------------ product_sections[T1,T2:TYPE]: THEORY BEGIN X,Y: VAR set[[T1,T2]] a: VAR T1 b: VAR T2 IMPORTING topology@cross_product[T1,T2] x_section_emptyset: LEMMA x_section(emptyset,a) = emptyset x_section_complement: LEMMA x_section(complement(X),a) = complement(x_section(X,a)) x_section_union: LEMMA x_section(union(X,Y),a) = union(x_section(X,a),x_section(Y,a)) x_section_intersection: LEMMA x_section(intersection(X,Y),a) = intersection(x_section(X,a),x_section(Y,a)) x_section_disjoint: LEMMA disjoint?(X,Y) => disjoint?(x_section(X,a),x_section(Y,a)) y_section_emptyset: LEMMA y_section(emptyset,b) = emptyset y_section_complement: LEMMA y_section(complement(X),b) = complement(y_section(X,b)) y_section_union: LEMMA y_section(union(X,Y),b) = union(y_section(X,b),y_section(Y,b)) y_section_intersection: LEMMA y_section(intersection(X,Y),b) = intersection(y_section(X,b),y_section(Y,b)) y_section_disjoint: LEMMA disjoint?(X,Y) => disjoint?(y_section(X,b),y_section(Y,b)) END product_sections ¤ 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.0.11Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28