| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle integral_diff_doms.pvs Sprache: PVS |
|||||||||
|
integral_diff_doms[T: TYPE+ FROM real, U: TYPE+ FROM real]: THEORY
%---------------------------------------------------------------------------- % % Integral of two functions that are identical over the integration % range and have different domains are shown to be equal. % % Author: Rick Butler NASA Langley Research Center % %---------------------------------------------------------------------------- BEGIN ASSUMING IMPORTING deriv_domain_def connected_domain : ASSUMPTION connected?[T] not_one_element : ASSUMPTION not_one_element?[T] con_dom_U : ASSUMPTION connected?[U] not_one_U : ASSUMPTION not_one_element?[U] ENDASSUMING IMPORTING integral f: VAR [T -> real] g: VAR [U -> real] a,b: VAR real int_diff_dom: LEMMA T_pred(a) AND T_pred(b) AND U_pred(a) AND U_pred(b) AND a < b AND integrable?[T](a,b,f) AND integrable?[U](a, b, g) AND (FORALL (x: real): x >= a AND x <= b IMPLIES f(x) = g(x)) IMPLIES integral(a,b,f) = integral(a,b,g) Int_diff_dom: LEMMA T_pred(a) AND T_pred(b) AND U_pred(a) AND U_pred(b) AND Integrable?[T](a,b,f) AND Integrable?[U](a, b, g) AND (FORALL (x: Closed_interval[real](a,b)): f(x) = g(x)) IMPLIES Integral(a,b,f) = Integral(a,b,g) END integral_diff_doms ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28