| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/lebesgue/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle restriction_integral.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Extras for analysis library % % Author: David Lester, Manchester University % % (Bored at Houston, after SCAN08 in El Paso) % % Version 1.0 26/2/10 Initial Version %------------------------------------------------------------------------------ restriction_integral[T1,T2:TYPE FROM real]: THEORY BEGIN ASSUMING connected_domain_T1 : ASSUMPTION FORALL (x, y : T1), (z : real) : x <= z AND z <= y IMPLIES T1_pred(z) connected_domain_T2 : ASSUMPTION FORALL (x, y : T2), (z : real) : x <= z AND z <= y IMPLIES T2_pred(z) not_one_element_T1 : ASSUMPTION FORALL (x : T1) : EXISTS (y : T1) : x /= y not_one_element_T2 : ASSUMPTION FORALL (x : T2) : EXISTS (y : T2) : x /= y sub_domain : ASSUMPTION FORALL (x : T1) : EXISTS (y : T2) : x = y ENDASSUMING IMPORTING analysis@integral_def a,b: VAR T1 c: VAR real f: VAR [T2 -> real] g: VAR [T1 -> real] restrict_Integrable: LEMMA Integrable?[T2](a,b,f) <=> Integrable?[T1](a,b,restrict[T2,T1,real](f)) restrict_Integral: LEMMA Integrable?[T2](a,b,f) => Integral[T2](a,b,f) = Integral[T1](a,b,restrict[T2,T1,real](f)) extend_Integrable: LEMMA Integrable?[T1](a,b,g) <=> Integrable?[T2](a,b,extend[T2,T1,real,c](g)) extend_Integral: LEMMA Integrable?[T1](a,b,g) => Integral[T1](a,b,g) = Integral[T2](a,b,extend[T2,T1,real,c](g)) END restriction_integral ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28