%------------------------------------------------------------------------------
% Subspace Continuity
%
% Continuity is preserved on subspaces
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            8/10/04  Initial Version
%     Version 1.1            9/06/06  Changed interface, added Type Judgements
%------------------------------------------------------------------------------

continuity_subspace[T1:TYPE, (IMPORTING topology_def[T1]) S:topology[T1],
                    T2:TYPE, (IMPORTING topology_def[T2]) T:topology[T2],
                    T3:TYPE FROM T1]: THEORY

BEGIN

  IMPORTING subspace[T1,S,T3],
            continuity[T1,S,T2,T],
            continuity

  x: VAR T3
  f: VAR [T1->T2]

  subspace_continuous_at: LEMMA continuous_at?(f,x) =>
              continuous_at?[T3,induced_topology,T2,T](restrict[T1,T3,T2](f),x)

  subspace_continuous: LEMMA continuous?(f) =>
        continuous?[T3,induced_topology,T2,T](restrict[T1,T3,T2](f))

  F: VAR continuous[T1,S,T2,T]

  restrict_is_continuous:
    JUDGEMENT restrict[T1,T3,T2](F) HAS_TYPE
                                           continuous[T3,induced_topology,T2,T]

END continuity_subspace