| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/Tools/Nunchaku/ (Columbo Version 0.7©) Datei vom 16.11.2025 mit Größe 41 kB |
|
Quelle metric_def.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Metric Spaces Definitions % % 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 %------------------------------------------------------------------------------ metric_def[T:TYPE]: THEORY BEGIN x,y,z: VAR T d: VAR [T,T->nnreal] metric_zero?(d) :bool = FORALL x,y: d(x,y) = 0 <=> x = y metric_symmetric?(d):bool = FORALL x,y: d(x,y) = d(y,x) metric_triangle?(d) :bool = FORALL x,y,z: d(x,z) <= d(x,y) + d(y,z) metric?(d):bool = metric_zero?(d) AND metric_symmetric?(d) AND metric_triangle?(d) discrete_metric(x,y):[nnreal] = IF x = y THEN 0 ELSE 1 ENDIF metric: TYPE+ = (metric?) CONTAINING discrete_metric discrete_metric_is_metric: JUDGEMENT discrete_metric HAS_TYPE metric END metric_def ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28