| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 827 B |
|
Quelle real_fun_continuity_equiv.pvs Sprache: PVS |
|||||||||
|
real_fun_continuity_equiv: THEORY
%------------------------------------------------------------------------------ % There are two definitions of continuity of functions real -> real. One is % based on metric spaces and the other is a direct definition. In this theory, % we prove the equivalence of these definitions. % % Authors: Anthony Narkawicz, NASA Langley % % Version 1.0 10/9/2009 Initial Version %------------------------------------------------------------------------------ BEGIN IMPORTING real_metric_space, continuous_functions, continuity_ms_def f: VAR [real -> real] continuous_real : TYPE = {f | continuous?[real](f)} real_fun_continuity_equiv: LEMMA continuous?[real,real_dist,real,real_dist](f) IFF continuous?[real](f) END real_fun_continuity_equiv ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28