let I be non empty set ; :: thesis: for T being Scott TopAugmentation of product (I --> (BoolePoset 1)) holds the topology of T = the topology of (product (I --> Sierpinski_Space ))
let T be Scott TopAugmentation of product (I --> (BoolePoset 1)); :: thesis: the topology of T = the topology of (product (I --> Sierpinski_Space ))
A1:
RelStr(# the carrier of T,the InternalRel of T #) = product (I --> (BoolePoset 1))
by YELLOW_9:def 4;
set IB = I --> (BoolePoset 1);
set IS = I --> Sierpinski_Space ;
LattPOSet (BooleLatt 1) = RelStr(# the carrier of (BooleLatt 1),(LattRel (BooleLatt 1)) #)
by LATTICE3:def 2;
then A2: the carrier of (BoolePoset 1) =
the carrier of (BooleLatt 1)
by YELLOW_1:def 2
.=
bool {{} }
by CARD_1:87, LATTICE3:def 1
.=
{0 ,1}
by CARD_1:87, ZFMISC_1:30
;
A3: dom (Carrier (I --> (BoolePoset 1))) =
I
by PARTFUN1:def 4
.=
dom (Carrier (I --> Sierpinski_Space ))
by PARTFUN1:def 4
;
A4:
for i being set st i in dom (Carrier (I --> (BoolePoset 1))) holds
(Carrier (I --> (BoolePoset 1))) . i = (Carrier (I --> Sierpinski_Space )) . i
then A10:
Carrier (I --> (BoolePoset 1)) = Carrier (I --> Sierpinski_Space )
by A3, FUNCT_1:9;
A11: the carrier of T =
product (Carrier (I --> (BoolePoset 1)))
by A1, YELLOW_1:def 4
.=
product (Carrier (I --> Sierpinski_Space ))
by A3, A4, FUNCT_1:9
.=
the carrier of (product (I --> Sierpinski_Space ))
by Def3
;
A12:
the carrier of (product (I --> (BoolePoset 1))) = product (Carrier (I --> (BoolePoset 1)))
by YELLOW_1:def 4;
reconsider P = { (product ((Carrier (I --> Sierpinski_Space )) +* ii,{1})) where ii is Element of I : verum } as prebasis of product (I --> Sierpinski_Space ) by Th14;
reconsider T' = T as complete Scott TopLattice ;
T' is algebraic
by A1, WAYBEL_8:17;
then consider R being Basis of T' such that
A13:
R = { (uparrow yy) where yy is Element of T' : yy in the carrier of (CompactSublatt T') }
by WAYBEL14:42;
consider f being Function of (BoolePoset I),(product (I --> (BoolePoset 1))) such that
A14:
f is isomorphic
and
A15:
for Y being Subset of I holds f . Y = chi Y,I
by Th15;
A16:
rng f = the carrier of (product (I --> (BoolePoset 1)))
by A14, WAYBEL_0:66;
A17:
R c= FinMeetCl P
proof
let X be
set ;
:: according to TARSKI:def 3 :: thesis: ( not X in R or X in FinMeetCl P )
assume A18:
X in R
;
:: thesis: X in FinMeetCl P
then consider Y being
Element of
T' such that A19:
X = uparrow Y
and A20:
Y in the
carrier of
(CompactSublatt T')
by A13;
A21:
Y is
compact
by A20, WAYBEL_8:def 1;
reconsider X' =
X as
Subset of
(product (I --> Sierpinski_Space )) by A11, A18;
reconsider y =
Y as
Element of
(product (I --> (BoolePoset 1))) by A1;
A22:
y is
compact
by A1, A21, WAYBEL_8:9;
consider x being
set such that A23:
x in dom f
and A24:
y = f . x
by A16, FUNCT_1:def 5;
reconsider x =
x as
Element of
(BoolePoset I) by A23;
reconsider x' =
x as
Subset of
I by WAYBEL_8:28;
deffunc H1(
Element of
I)
-> set =
product ((Carrier (I --> Sierpinski_Space )) +* $1,{1});
x is
compact
by A14, A22, A24, WAYBEL13:28;
then A25:
x is
finite
by WAYBEL_8:30;
A26:
uparrow Y =
uparrow {Y}
by WAYBEL_0:def 18
.=
uparrow {y}
by A1, WAYBEL_0:13
.=
uparrow y
by WAYBEL_0:def 18
;
set ZZ =
{ (product ((Carrier (I --> Sierpinski_Space )) +* jj,{1})) where jj is Element of I : jj in x } ;
A27:
{ (product ((Carrier (I --> Sierpinski_Space )) +* jj,{1})) where jj is Element of I : jj in x } c= P
then reconsider ZZ =
{ (product ((Carrier (I --> Sierpinski_Space )) +* jj,{1})) where jj is Element of I : jj in x } as
Subset-Family of
(product (I --> Sierpinski_Space )) by XBOOLE_1:1;
A29:
{ H1(jj) where jj is Element of I : jj in x } is
finite
from FRAENKEL:sch 21(A25);
A30:
X' c= Intersect ZZ
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in X' or z in Intersect ZZ )
assume A31:
z in X'
;
:: thesis: z in Intersect ZZ
then A32:
z in the
carrier of
(product (I --> (BoolePoset 1)))
by A1, A11;
reconsider z' =
z as
Element of
(product (I --> (BoolePoset 1))) by A1, A11, A31;
z in product (Carrier (I --> (BoolePoset 1)))
by A32, YELLOW_1:def 4;
then consider gg being
Function such that A33:
z = gg
and A34:
dom gg = dom (Carrier (I --> (BoolePoset 1)))
and A35:
for
w being
set st
w in dom (Carrier (I --> (BoolePoset 1))) holds
gg . w in (Carrier (I --> (BoolePoset 1))) . w
by CARD_3:def 5;
y <= z'
by A19, A26, A31, WAYBEL_0:18;
then consider h1,
h2 being
Function such that A36:
h1 = y
and A37:
h2 = z'
and A38:
for
i being
set st
i in I holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = (I --> (BoolePoset 1)) . i &
xi = h1 . i &
yi = h2 . i &
xi <= yi )
by A12, YELLOW_1:def 4;
A39:
h1 =
f . x'
by A24, A36
.=
chi x,
I
by A15
;
for
Z being
set st
Z in ZZ holds
z in Z
proof
let Z be
set ;
:: thesis: ( Z in ZZ implies z in Z )
assume
Z in ZZ
;
:: thesis: z in Z
then consider j being
Element of
I such that A40:
Z = product ((Carrier (I --> Sierpinski_Space )) +* j,{1})
and A41:
j in x
;
A42:
dom ((Carrier (I --> Sierpinski_Space )) +* j,{1}) =
dom (Carrier (I --> Sierpinski_Space ))
by FUNCT_7:32
.=
I
by PARTFUN1:def 4
;
consider RS being
RelStr ,
xj,
yj being
Element of
RS such that A43:
RS = (I --> (BoolePoset 1)) . j
and A44:
xj = h1 . j
and A45:
yj = h2 . j
and A46:
xj <= yj
by A38;
A47:
xj = 1
by A39, A41, A44, FUNCT_3:def 3;
reconsider a =
xj,
b =
yj as
Element of
(BoolePoset 1) by A43, FUNCOP_1:13;
A48:
a <= b
by A43, A46, FUNCOP_1:13;
A49:
b in the
carrier of
(BoolePoset 1)
;
A50:
yj <> 0
A52:
dom h2 = dom ((Carrier (I --> Sierpinski_Space )) +* j,{1})
by A33, A34, A37, A42, PARTFUN1:def 4;
for
w being
set st
w in dom ((Carrier (I --> Sierpinski_Space )) +* j,{1}) holds
h2 . w in ((Carrier (I --> Sierpinski_Space )) +* j,{1}) . w
hence
z in Z
by A37, A40, A52, CARD_3:def 5;
:: thesis: verum
end;
hence
z in Intersect ZZ
by A31, SETFAM_1:58;
:: thesis: verum
end;
Intersect ZZ c= X'
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in Intersect ZZ or z in X' )
assume A56:
z in Intersect ZZ
;
:: thesis: z in X'
then A57:
z in the
carrier of
(product (I --> (BoolePoset 1)))
by A1, A11;
reconsider z' =
z as
Element of
(product (I --> (BoolePoset 1))) by A1, A11, A56;
set h1 =
chi x,
I;
A58:
chi x,
I =
f . x'
by A15
.=
y
by A24
;
z in product (Carrier (I --> (BoolePoset 1)))
by A57, YELLOW_1:def 4;
then consider h2 being
Function such that A59:
z = h2
and
dom h2 = dom (Carrier (I --> (BoolePoset 1)))
and A60:
for
w being
set st
w in dom (Carrier (I --> (BoolePoset 1))) holds
h2 . w in (Carrier (I --> (BoolePoset 1))) . w
by CARD_3:def 5;
for
i being
set st
i in I holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = (I --> (BoolePoset 1)) . i &
xi = (chi x,I) . i &
yi = h2 . i &
xi <= yi )
proof
let i be
set ;
:: thesis: ( i in I implies ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset 1)) . i & xi = (chi x,I) . i & yi = h2 . i & xi <= yi ) )
assume A61:
i in I
;
:: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset 1)) . i & xi = (chi x,I) . i & yi = h2 . i & xi <= yi )
then reconsider i' =
i as
Element of
I ;
take RS =
BoolePoset 1;
:: thesis: ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi x,I) . i & yi = h2 . i & xi <= yi )
consider RB being
1-sorted such that A62:
RB = (I --> (BoolePoset 1)) . i
and A63:
(Carrier (I --> (BoolePoset 1))) . i = the
carrier of
RB
by A61, PRALG_1:def 13;
A64:
(Carrier (I --> (BoolePoset 1))) . i = {0 ,1}
by A2, A61, A62, A63, FUNCOP_1:13;
A65:
i in dom (Carrier (I --> (BoolePoset 1)))
by A61, PARTFUN1:def 4;
then A66:
h2 . i in (Carrier (I --> (BoolePoset 1))) . i
by A60;
per cases
( i in x or not i in x )
;
suppose A67:
i in x
;
:: thesis: ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi x,I) . i & yi = h2 . i & xi <= yi )then
product ((Carrier (I --> Sierpinski_Space )) +* i',{1}) in ZZ
;
then
z in product ((Carrier (I --> Sierpinski_Space )) +* i',{1})
by A56, SETFAM_1:58;
then consider h2' being
Function such that A68:
z = h2'
and
dom h2' = dom ((Carrier (I --> Sierpinski_Space )) +* i',{1})
and A69:
for
w being
set st
w in dom ((Carrier (I --> Sierpinski_Space )) +* i',{1}) holds
h2' . w in ((Carrier (I --> Sierpinski_Space )) +* i',{1}) . w
by CARD_3:def 5;
i' in dom ((Carrier (I --> Sierpinski_Space )) +* i',{1})
by A3, A65, FUNCT_7:32;
then A70:
h2' . i' in ((Carrier (I --> Sierpinski_Space )) +* i',{1}) . i'
by A69;
A71:
((Carrier (I --> Sierpinski_Space )) +* i',{1}) . i' = {1}
by A3, A65, FUNCT_7:33;
reconsider xi = 1,
yi = 1 as
Element of
RS by A2, TARSKI:def 2;
take
xi
;
:: thesis: ex yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi x,I) . i & yi = h2 . i & xi <= yi )take
yi
;
:: thesis: ( RS = (I --> (BoolePoset 1)) . i & xi = (chi x,I) . i & yi = h2 . i & xi <= yi )thus
RS = (I --> (BoolePoset 1)) . i
by A61, FUNCOP_1:13;
:: thesis: ( xi = (chi x,I) . i & yi = h2 . i & xi <= yi )thus
xi = (chi x,I) . i
by A61, A67, FUNCT_3:def 3;
:: thesis: ( yi = h2 . i & xi <= yi )thus
yi = h2 . i
by A59, A68, A70, A71, TARSKI:def 1;
:: thesis: xi <= yithus
xi <= yi
;
:: thesis: verum end;
end;
then
y <= z'
by A12, A58, A59, YELLOW_1:def 4;
hence
z in X'
by A19, A26, WAYBEL_0:18;
:: thesis: verum
end;
then
X' = Intersect ZZ
by A30, XBOOLE_0:def 10;
hence
X in FinMeetCl P
by A27, A29, CANTOR_1:def 4;
:: thesis: verum
end;
FinMeetCl P c= R
proof
let X be
set ;
:: according to TARSKI:def 3 :: thesis: ( not X in FinMeetCl P or X in R )
assume A75:
X in FinMeetCl P
;
:: thesis: X in R
then reconsider X' =
X as
Subset of
(product (I --> Sierpinski_Space )) ;
consider ZZ being
Subset-Family of
(product (I --> Sierpinski_Space )) such that A76:
ZZ c= P
and A77:
ZZ is
finite
and A78:
X = Intersect ZZ
by A75, CANTOR_1:def 4;
deffunc H1(
set )
-> set =
product ((Carrier (I --> Sierpinski_Space )) +* $1,{1});
consider F being
Function such that A79:
dom F = I
and A80:
for
e being
set st
e in I holds
F . e = H1(
e)
from FUNCT_1:sch 3();
P c= rng F
then
ZZ c= rng F
by A76, XBOOLE_1:1;
then consider x' being
set such that A82:
x' c= dom F
and A83:
x' is
finite
and A84:
F .: x' = ZZ
by A77, ORDERS_1:195;
reconsider x' =
x' as
Subset of
I by A79, A82;
set PP =
{ (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : i in x' } ;
A85:
ZZ c= { (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : i in x' }
{ (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : i in x' } c= ZZ
then A91:
ZZ = { (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : i in x' }
by A85, XBOOLE_0:def 10;
reconsider x =
x' as
Element of
(BoolePoset I) by WAYBEL_8:28;
A92:
x is
compact
by A83, WAYBEL_8:30;
reconsider y =
f . x as
Element of
(product (I --> (BoolePoset 1))) ;
A93:
y is
compact
by A14, A92, WAYBEL13:28;
reconsider Y =
y as
Element of
T' by A1;
A94:
uparrow Y =
uparrow {Y}
by WAYBEL_0:def 18
.=
uparrow {y}
by A1, WAYBEL_0:13
.=
uparrow y
by WAYBEL_0:def 18
;
A95:
X' c= uparrow y
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in X' or z in uparrow y )
assume A96:
z in X'
;
:: thesis: z in uparrow y
then A97:
z in the
carrier of
(product (I --> (BoolePoset 1)))
by A1, A11;
reconsider z' =
z as
Element of
(product (I --> (BoolePoset 1))) by A1, A11, A96;
set h1 =
chi x,
I;
A98:
chi x,
I = y
by A15;
z in product (Carrier (I --> (BoolePoset 1)))
by A97, YELLOW_1:def 4;
then consider h2 being
Function such that A99:
z = h2
and
dom h2 = dom (Carrier (I --> (BoolePoset 1)))
and A100:
for
w being
set st
w in dom (Carrier (I --> (BoolePoset 1))) holds
h2 . w in (Carrier (I --> (BoolePoset 1))) . w
by CARD_3:def 5;
for
i being
set st
i in I holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = (I --> (BoolePoset 1)) . i &
xi = (chi x,I) . i &
yi = h2 . i &
xi <= yi )
proof
let i be
set ;
:: thesis: ( i in I implies ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset 1)) . i & xi = (chi x,I) . i & yi = h2 . i & xi <= yi ) )
assume A101:
i in I
;
:: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset 1)) . i & xi = (chi x,I) . i & yi = h2 . i & xi <= yi )
then reconsider i' =
i as
Element of
I ;
take RS =
BoolePoset 1;
:: thesis: ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi x,I) . i & yi = h2 . i & xi <= yi )
consider RB being
1-sorted such that A102:
RB = (I --> (BoolePoset 1)) . i
and A103:
(Carrier (I --> (BoolePoset 1))) . i = the
carrier of
RB
by A101, PRALG_1:def 13;
A104:
(Carrier (I --> (BoolePoset 1))) . i = {0 ,1}
by A2, A101, A102, A103, FUNCOP_1:13;
A105:
i in dom (Carrier (I --> (BoolePoset 1)))
by A101, PARTFUN1:def 4;
then A106:
h2 . i in (Carrier (I --> (BoolePoset 1))) . i
by A100;
per cases
( i in x or not i in x )
;
suppose A107:
i in x
;
:: thesis: ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi x,I) . i & yi = h2 . i & xi <= yi )then
product ((Carrier (I --> Sierpinski_Space )) +* i',{1}) in ZZ
by A91;
then
z in product ((Carrier (I --> Sierpinski_Space )) +* i',{1})
by A78, A96, SETFAM_1:58;
then consider h2' being
Function such that A108:
z = h2'
and
dom h2' = dom ((Carrier (I --> Sierpinski_Space )) +* i',{1})
and A109:
for
w being
set st
w in dom ((Carrier (I --> Sierpinski_Space )) +* i',{1}) holds
h2' . w in ((Carrier (I --> Sierpinski_Space )) +* i',{1}) . w
by CARD_3:def 5;
i' in dom ((Carrier (I --> Sierpinski_Space )) +* i',{1})
by A3, A105, FUNCT_7:32;
then A110:
h2' . i' in ((Carrier (I --> Sierpinski_Space )) +* i',{1}) . i'
by A109;
A111:
((Carrier (I --> Sierpinski_Space )) +* i',{1}) . i' = {1}
by A3, A105, FUNCT_7:33;
reconsider xi = 1,
yi = 1 as
Element of
RS by A2, TARSKI:def 2;
take
xi
;
:: thesis: ex yi being Element of RS st
( RS = (I --> (BoolePoset 1)) . i & xi = (chi x,I) . i & yi = h2 . i & xi <= yi )take
yi
;
:: thesis: ( RS = (I --> (BoolePoset 1)) . i & xi = (chi x,I) . i & yi = h2 . i & xi <= yi )thus
RS = (I --> (BoolePoset 1)) . i
by A101, FUNCOP_1:13;
:: thesis: ( xi = (chi x,I) . i & yi = h2 . i & xi <= yi )thus
xi = (chi x,I) . i
by A107, FUNCT_3:def 3;
:: thesis: ( yi = h2 . i & xi <= yi )thus
yi = h2 . i
by A99, A108, A110, A111, TARSKI:def 1;
:: thesis: xi <= yithus
xi <= yi
;
:: thesis: verum end;
end;
then
y <= z'
by A12, A98, A99, YELLOW_1:def 4;
hence
z in uparrow y
by WAYBEL_0:18;
:: thesis: verum
end;
uparrow y c= X'
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in uparrow y or z in X' )
assume A115:
z in uparrow y
;
:: thesis: z in X'
then A116:
z in the
carrier of
(product (I --> (BoolePoset 1)))
;
reconsider z' =
z as
Element of
(product (I --> (BoolePoset 1))) by A115;
z in product (Carrier (I --> (BoolePoset 1)))
by A116, YELLOW_1:def 4;
then consider gg being
Function such that A117:
z = gg
and A118:
dom gg = dom (Carrier (I --> (BoolePoset 1)))
and A119:
for
w being
set st
w in dom (Carrier (I --> (BoolePoset 1))) holds
gg . w in (Carrier (I --> (BoolePoset 1))) . w
by CARD_3:def 5;
y <= z'
by A115, WAYBEL_0:18;
then consider h1,
h2 being
Function such that A120:
h1 = y
and A121:
h2 = z'
and A122:
for
i being
set st
i in I holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = (I --> (BoolePoset 1)) . i &
xi = h1 . i &
yi = h2 . i &
xi <= yi )
by A12, YELLOW_1:def 4;
A123:
h1 = chi x,
I
by A15, A120;
for
Z being
set st
Z in ZZ holds
z in Z
proof
let Z be
set ;
:: thesis: ( Z in ZZ implies z in Z )
assume
Z in ZZ
;
:: thesis: z in Z
then consider j being
Element of
I such that A124:
Z = product ((Carrier (I --> Sierpinski_Space )) +* j,{1})
and A125:
j in x
by A91;
A126:
dom ((Carrier (I --> Sierpinski_Space )) +* j,{1}) =
dom (Carrier (I --> Sierpinski_Space ))
by FUNCT_7:32
.=
I
by PARTFUN1:def 4
;
consider RS being
RelStr ,
xj,
yj being
Element of
RS such that A127:
RS = (I --> (BoolePoset 1)) . j
and A128:
xj = h1 . j
and A129:
yj = h2 . j
and A130:
xj <= yj
by A122;
A131:
xj = 1
by A123, A125, A128, FUNCT_3:def 3;
A132:
RS = BoolePoset 1
by A127, FUNCOP_1:13;
reconsider b =
yj as
Element of
(BoolePoset 1) by A127, FUNCOP_1:13;
A133:
b in the
carrier of
(BoolePoset 1)
;
A134:
yj <> 0
A136:
dom h2 = dom ((Carrier (I --> Sierpinski_Space )) +* j,{1})
by A117, A118, A121, A126, PARTFUN1:def 4;
for
w being
set st
w in dom ((Carrier (I --> Sierpinski_Space )) +* j,{1}) holds
h2 . w in ((Carrier (I --> Sierpinski_Space )) +* j,{1}) . w
hence
z in Z
by A121, A124, A136, CARD_3:def 5;
:: thesis: verum
end;
hence
z in X'
by A1, A11, A78, A115, SETFAM_1:58;
:: thesis: verum
end;
then A140:
X = uparrow Y
by A94, A95, XBOOLE_0:def 10;
Y is
compact
by A1, A93, WAYBEL_8:9;
then
Y in the
carrier of
(CompactSublatt T')
by WAYBEL_8:def 1;
hence
X in R
by A13, A140;
:: thesis: verum
end;
then A141:
R = FinMeetCl P
by A17, XBOOLE_0:def 10;
reconsider P' = P as Subset-Family of T by A11;
P' is prebasis of T
by A11, A141, YELLOW_9:23;
hence
the topology of T = the topology of (product (I --> Sierpinski_Space ))
by A11, YELLOW_9:26; :: thesis: verum