| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 929 B |
|
Quelle continuous_functions_more.pvs Sprache: PVS |
|||||||||
|
continuous_functions_more [ T : TYPE FROM real ] : THEORY
%---------------------------------------------------------------------------- % % Additions made by Ricky W. Butler NASA Langley % %---------------------------------------------------------------------------- BEGIN ASSUMING connected_domain : ASSUMPTION FORALL (x, y : T), (z : real) : x <= z AND z <= y IMPLIES T_pred(z) not_one_element : ASSUMPTION FORALL (x : T) : EXISTS (y : T) : x /= y ENDASSUMING IMPORTING continuous_functions[T], convergence_sequences f: VAR [T -> real] a,b,c: VAR T cn: VAR sequence[T] n: VAR nat convergence_fun_of : LEMMA convergence(cn,c) AND continuous?(f,c) IMPLIES % move to analysis convergence(LAMBDA n: f(cn(n)),f(c)) IMPORTING unif_cont_fun %% to maintain upward compatibility END continuous_functions_more ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28