| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/vect_analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 920 B |
|
Quelle vect2_cont_comp2.pvs Sprache: PVS |
|||||||||
|
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.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28