begin
definition
let M,
N be non
empty MetrStruct ;
func max-Prod2 (
M,
N)
-> strict MetrStruct means :
Def1:
( the
carrier of
it = [: the carrier of M, the carrier of N:] & ( for
x,
y being
Point of
it ex
x1,
y1 being
Point of
M ex
x2,
y2 being
Point of
N st
(
x = [x1,x2] &
y = [y1,y2] & the
distance of
it . (
x,
y)
= max (
( the distance of M . (x1,y1)),
( the distance of N . (x2,y2))) ) ) );
existence
ex b1 being strict MetrStruct st
( the carrier of b1 = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b1 ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of b1 . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) )
uniqueness
for b1, b2 being strict MetrStruct st the carrier of b1 = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b1 ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of b1 . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) & the carrier of b2 = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b2 ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of b2 . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) holds
b1 = b2
end;
::
deftheorem Def1 defines
max-Prod2 TOPREAL7:def 1 :
for M, N being non empty MetrStruct
for b3 being strict MetrStruct holds
( b3 = max-Prod2 (M,N) iff ( the carrier of b3 = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b3 ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of b3 . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) ) );
Lm1:
for M, N being non empty MetrSpace holds max-Prod2 (M,N) is discerning
Lm2:
for i, j being Element of NAT ex f being Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) st
( f is being_homeomorphism & ( for fi, fj being FinSequence st [fi,fj] in dom f holds
f . (fi,fj) = fi ^ fj ) )