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