let T1, T2 be TopSpace; :: thesis: ( not T1 is empty & not T2 is empty implies ( weight T1 c= weight [:T1,T2:] & weight T2 c= weight [:T1,T2:] ) )
defpred S1[ set ] means verum;
set PR2 = pr2 the carrier of T1,the carrier of T2;
set PR1 = pr1 the carrier of T1,the carrier of T2;
assume
( not T1 is empty & not T2 is empty )
; :: thesis: ( weight T1 c= weight [:T1,T2:] & weight T2 c= weight [:T1,T2:] )
then reconsider t1 = T1, t2 = T2 as non empty TopSpace ;
reconsider T12 = [:t1,t2:] as non empty TopSpace ;
consider B12 being Basis of T12 such that
A1:
card B12 = weight T12
by WAYBEL23:75;
defpred S2[ set ] means ( $1 in B12 & S1[$1] );
deffunc H1( Subset of T12) -> Element of bool the carrier of T1 = (pr1 the carrier of T1,the carrier of T2) .: $1;
consider B1 being Subset-Family of T1 such that
A2:
B1 = { H1(w) where w is Subset of T12 : S2[w] }
from LMOD_7:sch 5();
A3:
B12 c= the topology of T12
by CANTOR_1:def 2;
A4:
B1 c= the topology of T1
for A being Subset of T1 st A is open holds
for p being Point of T1 st p in A holds
ex a being Subset of T1 st
( a in B1 & p in a & a c= A )
proof
let A be
Subset of
T1;
:: thesis: ( A is open implies for p being Point of T1 st p in A holds
ex a being Subset of T1 st
( a in B1 & p in a & a c= A ) )
assume A7:
A is
open
;
:: thesis: for p being Point of T1 st p in A holds
ex a being Subset of T1 st
( a in B1 & p in a & a c= A )
A8:
[:A,([#] T2):] is
open
by A7, BORSUK_1:46;
set p2 = the
Point of
T2;
A9:
the
Point of
T2 in [#] t2
;
let p1 be
Point of
T1;
:: thesis: ( p1 in A implies ex a being Subset of T1 st
( a in B1 & p1 in a & a c= A ) )
assume A10:
p1 in A
;
:: thesis: ex a being Subset of T1 st
( a in B1 & p1 in a & a c= A )
A11:
[p1,the Point of T2] in [:A,([#] T2):]
by A9, A10, ZFMISC_1:106;
then reconsider p =
[p1,the Point of T2] as
Point of
T12 ;
consider a12 being
Subset of
T12 such that A12:
a12 in B12
and A13:
p in a12
and A14:
a12 c= [:A,([#] T2):]
by A8, A11, YELLOW_9:31;
(
p1 in [#] t1 & the
Point of
T2 in [#] t2 )
;
then A15:
(pr1 the carrier of T1,the carrier of T2) . p1,the
Point of
T2 = p1
by FUNCT_3:def 5;
a12 is
open
by A3, A12, PRE_TOPC:def 5;
then reconsider a =
H1(
a12) as
open Subset of
T1 by BORSUK_1:59;
take
a
;
:: thesis: ( a in B1 & p1 in a & a c= A )
dom (pr1 the carrier of T1,the carrier of T2) =
[:([#] T1),([#] T2):]
by FUNCT_3:def 5
.=
[#] T12
by BORSUK_1:def 5
;
hence
(
a in B1 &
p1 in a )
by A2, A12, A13, A15, FUNCT_1:def 12;
:: thesis: a c= A
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in a or y in A )
assume
y in a
;
:: thesis: y in A
then consider x being
set such that A16:
x in dom (pr1 the carrier of T1,the carrier of T2)
and A17:
(
x in a12 &
y = (pr1 the carrier of T1,the carrier of T2) . x )
by FUNCT_1:def 12;
consider x1,
x2 being
set such that A18:
(
x1 in [#] T1 &
x2 in [#] T2 )
and A19:
x = [x1,x2]
by A16, ZFMISC_1:def 2;
(pr1 the carrier of T1,the carrier of T2) . x1,
x2 = x1
by A18, FUNCT_3:def 5;
hence
y in A
by A14, A17, A19, ZFMISC_1:106;
:: thesis: verum
end;
then reconsider B1 = B1 as Basis of T1 by A4, YELLOW_9:32;
A20:
card { H1(w) where w is Subset of T12 : S2[w] } c= card B12
from BORSUK_2:sch 1();
weight t1 c= card B1
by WAYBEL23:74;
hence
weight T1 c= weight [:T1,T2:]
by A1, A2, A20, XBOOLE_1:1; :: thesis: weight T2 c= weight [:T1,T2:]
deffunc H2( Subset of T12) -> Element of bool the carrier of T2 = (pr2 the carrier of T1,the carrier of T2) .: $1;
consider B2 being Subset-Family of T2 such that
A21:
B2 = { H2(w) where w is Subset of T12 : S2[w] }
from LMOD_7:sch 5();
A22:
for A being Subset of T2 st A is open holds
for p being Point of T2 st p in A holds
ex a being Subset of T2 st
( a in B2 & p in a & a c= A )
proof
let A be
Subset of
T2;
:: thesis: ( A is open implies for p being Point of T2 st p in A holds
ex a being Subset of T2 st
( a in B2 & p in a & a c= A ) )
assume A23:
A is
open
;
:: thesis: for p being Point of T2 st p in A holds
ex a being Subset of T2 st
( a in B2 & p in a & a c= A )
A24:
[:([#] T1),A:] is
open
by A23, BORSUK_1:46;
set p1 = the
Point of
T1;
A25:
the
Point of
T1 in [#] t1
;
let p2 be
Point of
T2;
:: thesis: ( p2 in A implies ex a being Subset of T2 st
( a in B2 & p2 in a & a c= A ) )
assume A26:
p2 in A
;
:: thesis: ex a being Subset of T2 st
( a in B2 & p2 in a & a c= A )
A27:
[the Point of T1,p2] in [:([#] T1),A:]
by A25, A26, ZFMISC_1:106;
then reconsider p =
[the Point of T1,p2] as
Point of
T12 ;
consider a12 being
Subset of
T12 such that A28:
a12 in B12
and A29:
p in a12
and A30:
a12 c= [:([#] T1),A:]
by A24, A27, YELLOW_9:31;
( the
Point of
T1 in [#] t1 &
p2 in [#] t2 )
;
then A31:
(pr2 the carrier of T1,the carrier of T2) . the
Point of
T1,
p2 = p2
by FUNCT_3:def 6;
a12 is
open
by A3, A28, PRE_TOPC:def 5;
then reconsider a =
H2(
a12) as
open Subset of
T2 by BORSUK_1:59;
take
a
;
:: thesis: ( a in B2 & p2 in a & a c= A )
dom (pr2 the carrier of T1,the carrier of T2) =
[:([#] T1),([#] T2):]
by FUNCT_3:def 6
.=
[#] T12
by BORSUK_1:def 5
;
hence
(
a in B2 &
p2 in a )
by A21, A28, A29, A31, FUNCT_1:def 12;
:: thesis: a c= A
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in a or y in A )
assume
y in a
;
:: thesis: y in A
then consider x being
set such that A32:
x in dom (pr2 the carrier of T1,the carrier of T2)
and A33:
(
x in a12 &
y = (pr2 the carrier of T1,the carrier of T2) . x )
by FUNCT_1:def 12;
consider x1,
x2 being
set such that A34:
(
x1 in [#] T1 &
x2 in [#] T2 )
and A35:
x = [x1,x2]
by A32, ZFMISC_1:def 2;
(pr2 the carrier of T1,the carrier of T2) . x1,
x2 = x2
by A34, FUNCT_3:def 6;
hence
y in A
by A30, A33, A35, ZFMISC_1:106;
:: thesis: verum
end;
B2 c= the topology of T2
then reconsider B2 = B2 as Basis of T2 by A22, YELLOW_9:32;
A38:
card { H2(w) where w is Subset of T12 : S2[w] } c= card B12
from BORSUK_2:sch 1();
weight T2 c= card B2
by WAYBEL23:74;
hence
weight T2 c= weight [:T1,T2:]
by A1, A21, A38, XBOOLE_1:1; :: thesis: verum