|
%------------------------------------------------------------------------------
% (sub-) Metric Spaces
%
% Author: David Lester, Manchester University
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
% Version 1.0 17/08/07 Initial Version
%------------------------------------------------------------------------------
submetric_def[T1:TYPE, T2:TYPE FROM T1]: THEORY
BEGIN
IMPORTING metric_def[T1],
metric_def[T2]
d: VAR metric[T1]
submetric_is_metric?: LEMMA metric?[T2](restrict[[T1,T1],[T2,T2],nnreal](d))
submetric_is_metric: JUDGEMENT
restrict[[T1,T1],[T2,T2],nnreal](d) HAS_TYPE metric[T2]
END submetric_def
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
