begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem
theorem
theorem
theorem Th16:
theorem Th17:
theorem
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 ex
x1,
y1 being
Point of ex
x2,
y2 being
Point of 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 ex x1, y1 being Point of ex x2, y2 being Point of 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 ex x1, y1 being Point of ex x2, y2 being Point of 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 ex x1, y1 being Point of ex x2, y2 being Point of 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 ex
x1,
y1 being
Point of ex
x2,
y2 being
Point of 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) ) ) ) );
theorem
canceled;
theorem Th20:
theorem
theorem Th22:
Lm1:
for M, N being non empty MetrSpace holds max-Prod2 M,N is discerning
theorem Th23:
theorem Th24:
theorem Th25:
theorem
theorem