|
%------------------------------------------------------------------------------
% Subspaces of metric spaces
%
% Author: David Lester, Manchester University
%
% Version 1.0 17/08/07 Initial Version
%------------------------------------------------------------------------------
metric_subspace[T:TYPE, S: TYPE FROM T,
(IMPORTING metric_def[T]) d:metric]: THEORY
BEGIN
IMPORTING metric_def[T],
topology@topology_def[T],
metric_space_def[T,d],
metric_space_def[S,(restrict[[T,T],[S,S],nnreal](d))],
metric_space[T,d],
metric_space[S,(restrict[[T,T],[S,S],nnreal](d))],
topology@hausdorff_convergence[T,metric_induced_topology[T,d]]
complete_subspace: LEMMA % RKB 6.1.29(2)
metric_complete?[T,d](fullset[T]) AND metric_closed?[T,d](fullset[S]) =>
metric_complete?[S,(restrict[[T,T],[S,S],nnreal](d))](fullset[S])
END metric_subspace
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
