| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 876 B |
|
SSL fundamental_theorem.pvs Sprache: PVS |
|||||||||
|
fundamental_theorem[T: TYPE+ FROM real]: THEORY
%------------------------------------------------------------------------------ % % Theory and proofs taken from Introduction to Analysis (Maxwell Rosenlight) % % Author: Rick Butler NASA Langley % % Note: some material moved to theory indefinite_integral on 7/20/07 % %------------------------------------------------------------------------------ BEGIN ASSUMING IMPORTING deriv_domain_def[T] connected_domain : ASSUMPTION connected?[T] not_one_element : ASSUMPTION not_one_element?[T] ENDASSUMING IMPORTING deriv_domain_def deriv_domain: LEMMA deriv_domain?[T] IMPORTING integral, derivative_props[T] %, derivatives_more[T] a,b,c,x: VAR T f,F,G: VAR [T -> real] % NOTE: LEMMA "continuous_Integrable?[T]" implicitly used throughout fundamental: THEOREM continuous?(f) AND (FORALL x: F(x) = Integral(a,x,f)) IMPLIES derivable?(F) AND deriv(F) = f fundamental2: THEOREM continuous?(f) IMPLIES (EXISTS F: derivable?(F) AND deriv(F) = f) fundamental3: THEOREM derivable?(F) AND deriv(F) = f AND continuous?(f) IMPLIES Integrable?(a,b,f) AND Integral(a,b,f) = F(b) - F(a) derivable_Integrable?: COROLLARY derivable?(f) IMPLIES Integrable?(a,b,f) fundamental3b: COROLLARY derivable?(F) AND continuous?(deriv(F)) IMPLIES Integrable?(a,b,deriv(F)) AND Integral(a,b,deriv(F)) = F(b) - F(a) END fundamental_theorem ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28