|
%--------------------------------------------------------------------------------------------------
%
% 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]]: THEORY
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.20 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
