|
%------------------------------------------------------------------------------------------------
%
% 3-dimensional record-vectors form a metric space
%
% Author: Anthony Narkawicz, NASA Langley
%
%
% Version 1.0 September 16, 2009
%
%------------------------------------------------------------------------------------------------
vect3_metric_space: THEORY
BEGIN
IMPORTING vectors@distance_3D,analysis@metric_spaces[Vect3,dist]
S: VAR set[Vect3]
vect3_subset_metric_space : THEOREM metric_space?[Vect3,dist](S)
vect3_metric_space : COROLLARY metric_space?[Vect3,dist](fullset[Vect3])
END vect3_metric_space
¤ Dauer der Verarbeitung: 0.4 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.
|
