Quelle  submetric_def.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% (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