| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/probability/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 889 B |
|
Quelle continuous_functions_aux.pvs Sprache: PVS |
|||||||||
|
continuous_functions_aux[T : TYPE FROM real] : THEORY
BEGIN f : VAR [T -> real] x, x0 : VAR T n: VAR nat epsilon, delta: VAR posreal IMPORTING analysis@continuous_functions[T], analysis@convergence_ops right_continuous?(f,x0): bool = FORALL epsilon: EXISTS delta: FORALL x: x0 <= x AND x - x0 < delta IMPLIES abs(f(x) - f(x0)) < epsilon left_continuous?(f,x0): bool = FORALL epsilon: EXISTS delta: FORALL x: x <= x0 AND x0 - x < delta IMPLIES abs(f(x) - f(x0)) < epsilon right_continuous?(f): bool = FORALL x0 : right_continuous?(f, x0) left_continuous?(f): bool = FORALL x0 : left_continuous?(f, x0) continuous_lr_def: LEMMA continuous?(f) IFF right_continuous?(f) AND left_continuous?(f) END continuous_functions_aux ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28