| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/IMP/ (Beweissystem der NASA Version 6.0.9©) Datei vom 16.11.2025 mit Größe 9 kB |
|
Impressum 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] a,b,c,x: VAR T f,F,G: VAR [T -> real] % NOTE: LEMMA "continuous_Integrable?[T]" implicitly used throughout fundamental: AXIOM 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: AXIOM 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 ¤ 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.12Bemerkung: (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
