|
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.24 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
