%------------------------------------------------------------------------------
% Metric Continuity
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            20/3/07  Initial Version
%------------------------------------------------------------------------------

metric_continuity[T1:TYPE, (IMPORTING metric_def[T1]) d1:metric[T1],
                  T2:TYPE, (IMPORTING metric_def[T2]) d2:metric[T2]]:THEORY

BEGIN

  IMPORTING metric_space[T1,d1],
            metric_space[T2,d2],
            topology@topology_def[T1],
            topology@topology_def[T2],
            topology@topology[T1,metric_induced_topology[T1,d1]],
            topology@topology[T2,metric_induced_topology[T2,d2]],
            topology@hausdorff_convergence[T1,metric_induced_topology[T1,d1]],
            topology@hausdorff_convergence[T2,metric_induced_topology[T2,d2]],
            topology@continuity_def[T1,metric_induced_topology[T1,d1],
                                    T2,metric_induced_topology[T2,d2]],
            topology@continuity[T1,metric_induced_topology[T1,d1],
                                T2,metric_induced_topology[T2,d2]]

  f:             VAR [T1->T2]
  x,x0:          VAR T1
  u:             VAR sequence[T1]
  epsilon,delta: VAR posreal

  metric_continuous_at?(f,x0):bool
     = FORALL epsilon: EXISTS delta: FORALL x:
           member(x,ball(x0,delta)) => member(f(x),ball(f(x0),epsilon))

  metric_continuous?(f):bool = FORALL x: metric_continuous_at?(f,x)

  metric_continuous_at_def: LEMMA 
     continuous_at?(f,x0) <=> metric_continuous_at?(f,x0)

  metric_continuous_def: LEMMA
     continuous?(f) <=> metric_continuous?(f)

  metric_continuity_limit: LEMMA
     convergence?(u,x) AND metric_continuous_at?(f,x) =>
     convergence?(f o u, f(x))

  metric_continuous: TYPE = (metric_continuous?)

  metric_continuous_is_continuous:
                            JUDGEMENT metric_continuous SUBTYPE_OF continuous

  continuous_is_metric_continuous:
                            JUDGEMENT continuous SUBTYPE_OF metric_continuous

  uniform_continuous?(f):bool =
     (FORALL epsilon: EXISTS delta: FORALL x,x0:
                  member(x,ball(x0,delta)) => member(f(x),ball(f(x0),epsilon)))

  uniform_continuous: LEMMA uniform_continuous?(f) => continuous?(f)

  uniform_continuous: TYPE = (uniform_continuous?)

  uniform_continuous_is_continuous:
         JUDGEMENT uniform_continuous SUBTYPE_OF continuous

  IMPORTING  finite_sets@finite_sets_minmax[posreal,<=] % proof only

  compact_uniform_continuous: LEMMA
     compact_subset?(metric_induced_topology[T1,d1],fullset[T1]) =>
              (continuous?(f) <=> uniform_continuous?(f))

END metric_continuity