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