Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: TestG1ConcurrentModeFailureEvent.java 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.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.