%------------------------------------------------------------------------------
% Linking metric continuity to that in analysis, for T from real.
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            15/06/09  Initial Version
%------------------------------------------------------------------------------
continuity_link[T: TYPE FROM real]: THEORY

BEGIN

  IMPORTING analysis@continuous_functions[T],
            metric_space_def[real,(LAMBDA (x,y:real): abs(x-y))],
            metric_space[real,(LAMBDA (x,y:real): abs(x-y))],
            topology@continuity_subspace[real,metric_induced_topology,
                                         real,metric_induced_topology,T],
            metric_continuity[T,(lambda (x,y:T): abs(x-y)),
                              real,(LAMBDA (x,y:real): abs(x-y))]

  f: VAR [T->real]
  x: VAR T


   continuous_iff_continuous_at?: LEMMA
     continuous?[T](f,x) <=>
%RWB     continuous_at?[T,induced_topology,real,metric_induced_topology](f,x)
     continuous_at?[T, metric_induced_topology[T, (LAMBDA (x, y: T): abs(x - y))],
        real,
        metric_induced_topology
            [real, (LAMBDA (x, y: real): abs(x - y))]](f,x)

   continuous_iff_continuous?:    LEMMA
     continuous?[T](f)   <=>
 %RWB    continuous?[T,induced_topology,real,metric_induced_topology](f)
    continuous?[T, metric_induced_topology[T, (LAMBDA (x, y: T): abs(x - y))],
        real, metric_induced_topology
            [real, (LAMBDA (x, y: real): abs(x - y))]](f)

END continuity_link