|
%------------------------------------------------------------------------------
% 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
[ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
]
|
