| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Tools/VSCode/extension/media/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 262 B |
|
Quelle integral_cont.pvs 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 ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28