|
integral_cont[T: TYPE FROM real]: THEORY
%------------------------------------------------------------------------------
% Continuous functions are integrable
%
% Author: Rick Butler NASA Langley
%
%------------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING deriv_domain_def[T]
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
IMPORTING integral_cont_scaf[T],
continuous_functions
f: VAR [T -> real]
x,y,a,b: VAR T
in_interval : LEMMA FORALL (PP: partition(a,b)):
FORALL (ii : below(length(PP)-1)):
(FORALL (x, y: closed_interval(seq(PP)(ii), seq(PP)(ii + 1))):
abs(x - y) <= seq(PP)(1 + ii) - seq(PP)(ii))
continuous_integrable: LEMMA a < b AND
(FORALL (x: closed_interval(a,b)): continuous?(f,x))
IMPLIES integrable?(a,b,f)
cont_fun_integrable: COROLLARY a < b AND continuous?(f)
IMPLIES integrable?(a,b,f)
END integral_cont
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
