|
%------------------------------------------------------------------------------
% Extras for analysis library
%
% Author: David Lester, Manchester University
%
% (Bored at Houston, after SCAN08 in El Paso)
%
% Version 1.0 26/2/10 Initial Version
%------------------------------------------------------------------------------
restriction_integral[T1,T2:TYPE FROM real]: THEORY
BEGIN
ASSUMING
connected_domain_T1 : ASSUMPTION
FORALL (x, y : T1), (z : real) :
x <= z AND z <= y IMPLIES T1_pred(z)
connected_domain_T2 : ASSUMPTION
FORALL (x, y : T2), (z : real) :
x <= z AND z <= y IMPLIES T2_pred(z)
not_one_element_T1 : ASSUMPTION
FORALL (x : T1) : EXISTS (y : T1) : x /= y
not_one_element_T2 : ASSUMPTION
FORALL (x : T2) : EXISTS (y : T2) : x /= y
sub_domain : ASSUMPTION
FORALL (x : T1) : EXISTS (y : T2) : x = y
ENDASSUMING
IMPORTING analysis@integral_def
a,b: VAR T1
c: VAR real
f: VAR [T2 -> real]
g: VAR [T1 -> real]
restrict_Integrable: LEMMA Integrable?[T2](a,b,f) <=>
Integrable?[T1](a,b,restrict[T2,T1,real](f))
restrict_Integral: LEMMA Integrable?[T2](a,b,f) =>
Integral[T2](a,b,f) = Integral[T1](a,b,restrict[T2,T1,real](f))
extend_Integrable: LEMMA Integrable?[T1](a,b,g) <=>
Integrable?[T2](a,b,extend[T2,T1,real,c](g))
extend_Integral: LEMMA Integrable?[T1](a,b,g) =>
Integral[T1](a,b,g) = Integral[T2](a,b,extend[T2,T1,real,c](g))
END restriction_integral
¤ Dauer der Verarbeitung: 0.14 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.
|
