|
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)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
