Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Translator.tex
Sprache: PVS
|
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
[ zur Elbe Produktseite wechseln0.23Quellennavigators
Analyse erneut starten
]
|
|
