| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMPP/SSlibE2PP/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 1 kB |
|
Quelle lim_of_composition.pvs Sprache: PVS |
|||||||||
|
lim_of_composition [ T1, T2 : TYPE FROM real ] : THEORY
%---------------------------------------------------------------------------- % Author: Bruno Dutertre Royal Holloway & Bedford New College %---------------------------------------------------------------------------- BEGIN IMPORTING lim_of_functions, continuous_functions[T2] f : VAR [T1 -> T2] g : VAR [T2 -> real] x, y : VAR real z : VAR T2 l : VAR real adherence_lemma : LEMMA convergence(f, x, y) IMPLIES adh[T2](fullset[real])(y) adherence_lemma2 : LEMMA convergent?(f, x) IMPLIES adh[T2](fullset[real])(lim(f, x)) convergence_composition : LEMMA convergence(f, x, y) AND convergence(g, y, l) IMPLIES convergence(g o f, x, l) convergent_composition : LEMMA convergent?(f, x) AND convergent?(g, lim(f, x)) IMPLIES convergent?(g o f, x) lim_composition : LEMMA convergent?(f, x) AND convergent?(g, lim(f, x)) IMPLIES lim(g o f, x) = lim(g, lim(f, x)) convergence_comp_continuous: LEMMA convergence(f, x, z) AND continuous?(g, z) IMPLIES convergence(g o f, x, g(z)) convergent_comp_continuous : LEMMA convergent?(f, x) AND T2_pred(lim(f, x)) AND continuous?(g, lim(f, x)) IMPLIES convergent?(g o f, x) lim_comp_continuous : LEMMA convergent?(f, x) AND T2_pred(lim(f, x)) AND continuous?(g, lim(f, x)) IMPLIES lim(g o f, x) = g(lim(f, x)) END lim_of_composition ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28