|
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)
¤
|
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.
|
