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
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.0Bemerkung:
(vorverarbeitet)
¤
