Quelle  continuity_subspace.pvs

%------------------------------------------------------------------------------
% continuity on subspaces
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            15/06/09  Initial Version
%------------------------------------------------------------------------------
continuity_subspace[(IMPORTING metric_def)
                    T1:TYPE,d1:metric[T1],
                    T2:TYPE,d2:metric[T2],
                    T3:TYPE FROM T1]: THEORY

BEGIN

  IMPORTING
    metric_space[T1,d1],
    metric_space[T2,d2],
    topology@continuity_subspace[T1,metric_induced_topology[T1,d1],
                                 T2,metric_induced_topology[T2,d2],T3],
    topology@continuity_def[T3,induced_topology,
                            T2,metric_induced_topology[T2,d2]],
    metric_continuity[T3,(restrict[[T1,T1],[T3,T3],nnreal](d1)),T2,d2]

END continuity_subspace