| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/vect_analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 705 B |
|
Quelle vect_metric_space.pvs Sprache: 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 ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28