products/sources/formale sprachen/PVS/analysis/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei:   Sprache: PVS

Original von: 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.8 Sekunden  (vorverarbeitet)  ¤



zum Wurzelverzeichnis wechseln
Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt.
zum Wurzelverzeichnis wechseln
sprechenden Kalenders

in der Quellcodebibliothek suchen




Laden

Fehler beim Verzeichnis:


in der Quellcodebibliothek suchen

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff