let M, N be non empty MetrSpace; [:(TopSpaceMetr M),(TopSpaceMetr N):] = TopSpaceMetr (max-Prod2 (M,N))
set S = TopSpaceMetr M;
set T = TopSpaceMetr N;
A1:
TopSpaceMetr (max-Prod2 (M,N)) = TopStruct(# the carrier of (max-Prod2 (M,N)),(Family_open_set (max-Prod2 (M,N))) #)
by PCOMPS_1:def 5;
A2:
TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #)
by PCOMPS_1:def 5;
A3:
TopSpaceMetr N = TopStruct(# the carrier of N,(Family_open_set N) #)
by PCOMPS_1:def 5;
A4: the carrier of [:(TopSpaceMetr M),(TopSpaceMetr N):] =
[: the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr N):]
by BORSUK_1:def 2
.=
the carrier of (TopSpaceMetr (max-Prod2 (M,N)))
by A1, A2, A3, Def1
;
A5:
the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] = { (union A) where A is Subset-Family of [:(TopSpaceMetr M),(TopSpaceMetr N):] : A c= { [:X1,X2:] where X1 is Subset of (TopSpaceMetr M), X2 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & X2 in the topology of (TopSpaceMetr N) ) } }
by BORSUK_1:def 2;
the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] = the topology of (TopSpaceMetr (max-Prod2 (M,N)))
proof
thus
the
topology of
[:(TopSpaceMetr M),(TopSpaceMetr N):] c= the
topology of
(TopSpaceMetr (max-Prod2 (M,N)))
XBOOLE_0:def 10 the topology of (TopSpaceMetr (max-Prod2 (M,N))) c= the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):]proof
let X be
object ;
TARSKI:def 3 ( not X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] or X in the topology of (TopSpaceMetr (max-Prod2 (M,N))) )
assume A6:
X in the
topology of
[:(TopSpaceMetr M),(TopSpaceMetr N):]
;
X in the topology of (TopSpaceMetr (max-Prod2 (M,N)))
then consider A being
Subset-Family of
[:(TopSpaceMetr M),(TopSpaceMetr N):] such that A7:
X = union A
and A8:
A c= { [:X1,X2:] where X1 is Subset of (TopSpaceMetr M), X2 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & X2 in the topology of (TopSpaceMetr N) ) }
by A5;
for
x being
Point of
(max-Prod2 (M,N)) st
x in union A holds
ex
r being
Real st
(
r > 0 &
Ball (
x,
r)
c= union A )
proof
let x be
Point of
(max-Prod2 (M,N));
( x in union A implies ex r being Real st
( r > 0 & Ball (x,r) c= union A ) )
assume
x in union A
;
ex r being Real st
( r > 0 & Ball (x,r) c= union A )
then consider Z being
set such that A9:
x in Z
and A10:
Z in A
by TARSKI:def 4;
Z in { [:X1,X2:] where X1 is Subset of (TopSpaceMetr M), X2 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & X2 in the topology of (TopSpaceMetr N) ) }
by A8, A10;
then consider X1 being
Subset of
(TopSpaceMetr M),
X2 being
Subset of
(TopSpaceMetr N) such that A11:
Z = [:X1,X2:]
and A12:
X1 in the
topology of
(TopSpaceMetr M)
and A13:
X2 in the
topology of
(TopSpaceMetr N)
;
consider z1,
z2 being
object such that A14:
z1 in X1
and A15:
z2 in X2
and A16:
x = [z1,z2]
by A9, A11, ZFMISC_1:def 2;
reconsider z2 =
z2 as
Point of
N by A3, A15;
consider r2 being
Real such that A17:
r2 > 0
and A18:
Ball (
z2,
r2)
c= X2
by A3, A13, A15, PCOMPS_1:def 4;
reconsider z1 =
z1 as
Point of
M by A2, A14;
consider r1 being
Real such that A19:
r1 > 0
and A20:
Ball (
z1,
r1)
c= X1
by A2, A12, A14, PCOMPS_1:def 4;
take r =
min (
r1,
r2);
( r > 0 & Ball (x,r) c= union A )
thus
r > 0
by A19, A17, XXREAL_0:15;
Ball (x,r) c= union A
let b be
object ;
TARSKI:def 3 ( not b in Ball (x,r) or b in union A )
assume A21:
b in Ball (
x,
r)
;
b in union A
then reconsider bb =
b as
Point of
(max-Prod2 (M,N)) ;
A22:
dist (
bb,
x)
< r
by A21, METRIC_1:11;
consider x1,
y1 being
Point of
M,
x2,
y2 being
Point of
N such that A23:
bb = [x1,x2]
and A24:
x = [y1,y2]
and A25:
the
distance of
(max-Prod2 (M,N)) . (
bb,
x)
= max (
( the distance of M . (x1,y1)),
( the distance of N . (x2,y2)))
by Def1;
z2 = y2
by A16, A24, XTUPLE_0:1;
then
the
distance of
N . (
x2,
z2)
<= max (
( the distance of M . (x1,y1)),
( the distance of N . (x2,y2)))
by XXREAL_0:25;
then
(
min (
r1,
r2)
<= r2 & the
distance of
N . (
x2,
z2)
< r )
by A25, A22, XXREAL_0:2, XXREAL_0:17;
then
dist (
x2,
z2)
< r2
by XXREAL_0:2;
then A26:
x2 in Ball (
z2,
r2)
by METRIC_1:11;
z1 = y1
by A16, A24, XTUPLE_0:1;
then
the
distance of
M . (
x1,
z1)
<= max (
( the distance of M . (x1,y1)),
( the distance of N . (x2,y2)))
by XXREAL_0:25;
then
(
min (
r1,
r2)
<= r1 & the
distance of
M . (
x1,
z1)
< r )
by A25, A22, XXREAL_0:2, XXREAL_0:17;
then
dist (
x1,
z1)
< r1
by XXREAL_0:2;
then
x1 in Ball (
z1,
r1)
by METRIC_1:11;
then
b in [:X1,X2:]
by A20, A18, A23, A26, ZFMISC_1:87;
hence
b in union A
by A10, A11, TARSKI:def 4;
verum
end;
hence
X in the
topology of
(TopSpaceMetr (max-Prod2 (M,N)))
by A1, A4, A6, PCOMPS_1:def 4, A7;
verum
end;
let X be
object ;
TARSKI:def 3 ( not X in the topology of (TopSpaceMetr (max-Prod2 (M,N))) or X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):] )
assume A27:
X in the
topology of
(TopSpaceMetr (max-Prod2 (M,N)))
;
X in the topology of [:(TopSpaceMetr M),(TopSpaceMetr N):]
then reconsider Y =
X as
Subset of
[:(TopSpaceMetr M),(TopSpaceMetr N):] by A4;
A28:
Base-Appr Y = { [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( [:X1,Y1:] c= Y & X1 is open & Y1 is open ) }
by BORSUK_1:def 3;
A29:
union (Base-Appr Y) = Y
proof
thus
union (Base-Appr Y) c= Y
by BORSUK_1:12;
XBOOLE_0:def 10 Y c= union (Base-Appr Y)
let u be
object ;
TARSKI:def 3 ( not u in Y or u in union (Base-Appr Y) )
assume A30:
u in Y
;
u in union (Base-Appr Y)
then reconsider uu =
u as
Point of
(max-Prod2 (M,N)) by A1, A4;
consider r being
Real such that A31:
r > 0
and A32:
Ball (
uu,
r)
c= Y
by A1, A27, A30, PCOMPS_1:def 4;
uu in the
carrier of
(max-Prod2 (M,N))
;
then
uu in [: the carrier of M, the carrier of N:]
by Def1;
then consider u1,
u2 being
object such that A33:
u1 in the
carrier of
M
and A34:
u2 in the
carrier of
N
and A35:
u = [u1,u2]
by ZFMISC_1:def 2;
reconsider u2 =
u2 as
Point of
N by A34;
reconsider u1 =
u1 as
Point of
M by A33;
reconsider B2 =
Ball (
u2,
r) as
Subset of
(TopSpaceMetr N) by A3;
reconsider B1 =
Ball (
u1,
r) as
Subset of
(TopSpaceMetr M) by A2;
(
u1 in Ball (
u1,
r) &
u2 in Ball (
u2,
r) )
by A31, TBSP_1:11;
then A36:
u in [:B1,B2:]
by A35, ZFMISC_1:87;
A37:
[:B1,B2:] c= Y
proof
let x be
object ;
TARSKI:def 3 ( not x in [:B1,B2:] or x in Y )
assume
x in [:B1,B2:]
;
x in Y
then consider x1,
x2 being
object such that A38:
x1 in B1
and A39:
x2 in B2
and A40:
x = [x1,x2]
by ZFMISC_1:def 2;
reconsider x2 =
x2 as
Point of
N by A39;
reconsider x1 =
x1 as
Point of
M by A38;
consider p1,
p2 being
Point of
M,
q1,
q2 being
Point of
N such that A41:
(
uu = [p1,q1] &
[x1,x2] = [p2,q2] )
and A42:
the
distance of
(max-Prod2 (M,N)) . (
uu,
[x1,x2])
= max (
( the distance of M . (p1,p2)),
( the distance of N . (q1,q2)))
by Def1;
(
u2 = q1 &
x2 = q2 )
by A35, A41, XTUPLE_0:1;
then A43:
dist (
q1,
q2)
< r
by A39, METRIC_1:11;
(
u1 = p1 &
x1 = p2 )
by A35, A41, XTUPLE_0:1;
then
dist (
p1,
p2)
< r
by A38, METRIC_1:11;
then
dist (
uu,
[x1,x2])
< r
by A42, A43, XXREAL_0:16;
then
x in Ball (
uu,
r)
by A40, METRIC_1:11;
hence
x in Y
by A32;
verum
end;
(
B1 is
open &
B2 is
open )
by TOPMETR:14;
then
[:B1,B2:] in Base-Appr Y
by A28, A37;
hence
u in union (Base-Appr Y)
by A36, TARSKI:def 4;
verum
end;
Base-Appr Y c= { [:X1,Y1:] where X1 is Subset of (TopSpaceMetr M), Y1 is Subset of (TopSpaceMetr N) : ( X1 in the topology of (TopSpaceMetr M) & Y1 in the topology of (TopSpaceMetr N) ) }
hence
X in the
topology of
[:(TopSpaceMetr M),(TopSpaceMetr N):]
by A5, A29;
verum
end;
hence
[:(TopSpaceMetr M),(TopSpaceMetr N):] = TopSpaceMetr (max-Prod2 (M,N))
by A4; verum