Quelle  vect_metric_space.pvs

%------------------------------------------------------------------------------------------------
%
%       n-dimensional real vectors form a metric space
%
%       Author: Anthony Narkawicz, NASA Langley
%
%       
%       Version 1.0                     September 2, 2009
%
%------------------------------------------------------------------------------------------------


vect_metric_space[n: posnat]: THEORY
BEGIN

   IMPORTING vectors@distance[n],analysis@metric_spaces[Vector[n],dist]

   S: VAR set[Vector[n]]

   vectors_metric_space     : THEOREM metric_space?[Vector[n],dist](S)

   vect_subset_metric_space : COROLLARY metric_space?[Vector[n],dist](fullset[Vector[n]])


END vect_metric_space