| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle cross_metric_spaces.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------------
% % Product (Metric) Spaces % % Author: Anthony Narkawicz, NASA Langley % % % Version 1.0 August 19, 2009 % %------------------------------------------------------------------------------- cross_metric_spaces[T1:Type+,d1:[T1,T1->nnreal],T2:Type+,d2:[T2,T2->nnreal]]: THEOR BEGIN ASSUMING IMPORTING metric_spaces fullset_metric_space1: ASSUMPTION metric_space?[T1,d1](fullset[T1]) fullset_metric_space2: ASSUMPTION metric_space?[T2,d2](fullset[T2]) ENDASSUMING IMPORTING metric_spaces, reals@sqrt,reals@sq X,S: VAR set[T1] Y,T: VAR set[T2] x,y: VAR [T1,T2] z,w: VAR T2 d(x,y): nnreal = d1(x`1,y`1) + d2(x`2,y`2) product_is_metric: LEMMA metric_space?[[T1,T2],d](fullset[[T1,T2]]) d_square(x,y): nnreal = sqrt(sq(d1(x`1,y`1)) + sq(d2(x`2,y`2))) product_is_metric_square: LEMMA metric_space?[[T1,T2],d_square](fullset[[T1,T2]]) %% These to metrics produce equivalent topologies %% V,U: VAR set[[T1,T2]] % a quick lemma that will be used in the proof of the metric equivalence... euclic_linear_lemma: LEMMA FORALL (a,b,r: nnreal): sqrt(sq(a) + sq(b)) < r/2 implies a+b<r metric_equivalence: LEMMA open_in?[[T1,T2],d](V,U) IFF open_in?[[T1,T2],d_square](V,U) metric_equivalence2: COROLLARY open?[[T1,T2],d](V) IFF open?[[T1,T2],d_square](V) END cross_metric_spaces ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28