| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 909 B |
|
Quelle continuity_props.pvs Sprache: PVS |
|||||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Properties of continuous functions % % in relation with sequences, limits % % and points of accumulation % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% continuity_props[T : TYPE FROM real] : THEORY BEGIN IMPORTING continuous_functions, top_sequences f : VAR [T -> real] u : VAR sequence[T] l, a : VAR T %-------------------------------------------- % u is convergent to l and f is continuous %-------------------------------------------- continuity_limit : LEMMA convergence(u, l) AND continuous?(f, l) IMPLIES convergence(f o u, f(l)) %-------------------------------------------- % point of accumulation %-------------------------------------------- continuity_accumulation : LEMMA accumulation(u, a) AND continuous?(f, a) IMPLIES accumulation(f o u, f(a)) END continuity_props ¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28