|
vect2_cont_comp[T: TYPE FROM real]: THEORY
%------------------------------------------------------------------------------
%
% AUTHOR: Cesar Munoz NASA langley Research Center
% Rick Butler NASA langley Research Center
%
% Note that rT, frT could be generalized to [T1 -> T2], see vect2_cont_comp2
%
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING cont_vect2_real,
cont_vect2_vect2,
analysis@continuous_lambda[T],
cont_real_vect2[T]
fvv,fvv1,fvv2 : VAR [Vect2->Vect2]
fvr : VAR [Vect2->real]
fvT : VAR [Vect2->T]
frr : VAR [T->real]
frT : VAR [T->T]
frv : VAR [T->Vect2]
v,u : VAR Vect2
x,y : VAR T
nzx : VAR {t: T | t /= 0}
;o(fvv1,fvv2): [Vect2->Vect2] = LAMBDA (v): fvv1(fvv2(v))
;o(frv,fvT) : [Vect2->Vect2] = LAMBDA (v): frv(fvT(v))
;o(fvr,fvv) : [Vect2->real] = LAMBDA (v): fvr(fvv(v))
;o(frr,fvT) : [Vect2->real] = LAMBDA (v): frr(fvT(v))
;o(fvv,frv) : [T->Vect2] = LAMBDA (x): fvv(frv(x))
;o(frv,frT) : [T->Vect2] = LAMBDA (x): frv(frT(x))
;o(fvr,frv) : [T->real] = LAMBDA (x): fvr(frv(x))
vv,vv1,vv2 : VAR { f:[Vect2->Vect2] | continuous_vv?(f) }
vr : VAR { f:[Vect2->real] | continuous_vr?(f) }
vT : VAR { f:[Vect2->T] | continuous_vr?(f) }
rr : VAR { f:[T->real] | continuous?(f) }
rT : VAR { f:[T->T] | continuous?(f) }
rv,rv1,rv2 : VAR { f:[T->Vect2] | continuous_rv?(f) }
comp_vv_vv_cont : LEMMA
continuous_vv?(vv1 o vv2)
comp_rv_vr_cont : LEMMA
continuous_vv?(rv o vT)
comp_vr_vv_cont : LEMMA
continuous_vr?(vr o vv)
comp_rr_vr_cont : LEMMA
continuous_vr?(rr o vT)
comp_vv_rv_cont : LEMMA
continuous_rv?(vv o rv)
comp_rv_rr_cont : LEMMA
continuous_rv?(rv o rT)
comp_vr_rv_cont : LEMMA
continuous?(vr o rv)
END vect2_cont_comp
¤ Dauer der Verarbeitung: 0.29 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.
|
