|
vect2_cont_comp2[T1,T2: TYPE FROM real]: THEORY
%------------------------------------------------------------------------------
%
% Note that rT, frT could be generalized to [T1 -> T2]
% Perhaps this should be done in anotrher theory with importings T1,T2
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING cont_vect2_real,
cont_real_vect2
fvT : VAR [Vect2->T1]
ftt : VAR [T1->T2]
frv : VAR [T2->Vect2]
v: VAR Vect2
x: VAR T1
;o(ftt,fvT) : [Vect2->T2] = LAMBDA (v): ftt(fvT(v))
;o(frv,ftt) : [T1->Vect2] = LAMBDA (x): frv(ftt(x))
vT : VAR { f:[Vect2->T1] | continuous_vr?(f) }
tt : VAR { f:[T1->T2] | continuous?(f) }
rv : VAR { f:[T2->Vect2] | continuous_rv?(f) }
comp_tt_vt_cont : LEMMA
continuous_vr?(tt o vT)
comp_rv_tt_cont : LEMMA
continuous_rv?(rv o tt)
END vect2_cont_comp2
¤ Dauer der Verarbeitung: 0.17 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.
|
