let I be non empty set ; for T being Scott TopAugmentation of product (I --> (BoolePoset {0})) holds the topology of T = the topology of (product (I --> Sierpinski_Space))
set IB = I --> (BoolePoset {0});
set IS = I --> Sierpinski_Space;
A1:
the carrier of (product (I --> (BoolePoset {0}))) = product (Carrier (I --> (BoolePoset {0})))
by YELLOW_1:def 4;
LattPOSet (BooleLatt {0}) = RelStr(# the carrier of (BooleLatt {0}),(LattRel (BooleLatt {0})) #)
by LATTICE3:def 2;
then A2: the carrier of (BoolePoset {0}) =
the carrier of (BooleLatt {0})
by YELLOW_1:def 2
.=
bool {{}}
by LATTICE3:def 1
.=
{0,1}
by CARD_1:49, ZFMISC_1:24
;
A3:
for i being object st i in dom (Carrier (I --> (BoolePoset {0}))) holds
(Carrier (I --> (BoolePoset {0}))) . i = (Carrier (I --> Sierpinski_Space)) . i
reconsider P = { (product ((Carrier (I --> Sierpinski_Space)) +* (ii,{1}))) where ii is Element of I : verum } as prebasis of (product (I --> Sierpinski_Space)) by Th13;
let T be Scott TopAugmentation of product (I --> (BoolePoset {0})); the topology of T = the topology of (product (I --> Sierpinski_Space))
A9: dom (Carrier (I --> (BoolePoset {0}))) =
I
by PARTFUN1:def 2
.=
dom (Carrier (I --> Sierpinski_Space))
by PARTFUN1:def 2
;
reconsider T9 = T as complete Scott TopLattice ;
A10:
RelStr(# the carrier of T, the InternalRel of T #) = product (I --> (BoolePoset {0}))
by YELLOW_9:def 4;
then
T9 is algebraic
by WAYBEL_8:17;
then consider R being Basis of T9 such that
A11:
R = { (uparrow yy) where yy is Element of T9 : yy in the carrier of (CompactSublatt T9) }
by WAYBEL14:42;
A12: the carrier of T =
product (Carrier (I --> (BoolePoset {0})))
by A10, YELLOW_1:def 4
.=
product (Carrier (I --> Sierpinski_Space))
by A9, A3, FUNCT_1:2
.=
the carrier of (product (I --> Sierpinski_Space))
by Def3
;
then reconsider P9 = P as Subset-Family of T ;
consider f being Function of (BoolePoset I),(product (I --> (BoolePoset {0}))) such that
A13:
f is isomorphic
and
A14:
for Y being Subset of I holds f . Y = chi (Y,I)
by Th14;
A15:
Carrier (I --> (BoolePoset {0})) = Carrier (I --> Sierpinski_Space)
by A9, A3, FUNCT_1:2;
A16:
FinMeetCl P c= R
proof
deffunc H1(
object )
-> set =
product ((Carrier (I --> Sierpinski_Space)) +* ($1,{1}));
let X be
object ;
TARSKI:def 3 ( not X in FinMeetCl P or X in R )
consider F being
Function such that A17:
dom F = I
and A18:
for
e being
object st
e in I holds
F . e = H1(
e)
from FUNCT_1:sch 3();
assume A19:
X in FinMeetCl P
;
X in R
then reconsider X9 =
X as
Subset of
(product (I --> Sierpinski_Space)) ;
consider ZZ being
Subset-Family of
(product (I --> Sierpinski_Space)) such that A20:
ZZ c= P
and A21:
ZZ is
finite
and A22:
X = Intersect ZZ
by A19, CANTOR_1:def 3;
P c= rng F
then
ZZ c= rng F
by A20;
then consider x9 being
set such that A24:
x9 c= dom F
and A25:
x9 is
finite
and A26:
F .: x9 = ZZ
by A21, ORDERS_1:85;
reconsider x9 =
x9 as
Subset of
I by A17, A24;
reconsider x =
x9 as
Element of
(BoolePoset I) by WAYBEL_8:26;
reconsider y =
f . x as
Element of
(product (I --> (BoolePoset {0}))) ;
set PP =
{ (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9 } ;
A27:
ZZ c= { (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9 }
{ (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9 } c= ZZ
then A33:
ZZ = { (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : i in x9 }
by A27;
A34:
uparrow y c= X9
proof
let z be
object ;
TARSKI:def 3 ( not z in uparrow y or z in X9 )
assume A35:
z in uparrow y
;
z in X9
then reconsider z9 =
z as
Element of
(product (I --> (BoolePoset {0}))) ;
y <= z9
by A35, WAYBEL_0:18;
then consider h1,
h2 being
Function such that A36:
h1 = y
and A37:
h2 = z9
and A38:
for
i being
object st
i in I holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = (I --> (BoolePoset {0})) . i &
xi = h1 . i &
yi = h2 . i &
xi <= yi )
by A1, YELLOW_1:def 4;
z in the
carrier of
(product (I --> (BoolePoset {0})))
by A35;
then
z in product (Carrier (I --> (BoolePoset {0})))
by YELLOW_1:def 4;
then A39:
ex
gg being
Function st
(
z = gg &
dom gg = dom (Carrier (I --> (BoolePoset {0}))) & ( for
w being
object st
w in dom (Carrier (I --> (BoolePoset {0}))) holds
gg . w in (Carrier (I --> (BoolePoset {0}))) . w ) )
by CARD_3:def 5;
A40:
h1 = chi (
x,
I)
by A14, A36;
for
Z being
set st
Z in ZZ holds
z in Z
proof
let Z be
set ;
( Z in ZZ implies z in Z )
assume
Z in ZZ
;
z in Z
then consider j being
Element of
I such that A41:
Z = product ((Carrier (I --> Sierpinski_Space)) +* (j,{1}))
and A42:
j in x
by A33;
consider RS being
RelStr ,
xj,
yj being
Element of
RS such that A43:
RS = (I --> (BoolePoset {0})) . j
and A44:
xj = h1 . j
and A45:
yj = h2 . j
and A46:
xj <= yj
by A38;
A47:
RS = BoolePoset {0}
by A43;
A48:
xj = 1
by A40, A42, A44, FUNCT_3:def 3;
A49:
yj <> 0
reconsider b =
yj as
Element of
(BoolePoset {0}) by A43;
A50:
dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) =
dom (Carrier (I --> Sierpinski_Space))
by FUNCT_7:30
.=
I
by PARTFUN1:def 2
;
A51:
b in the
carrier of
(BoolePoset {0})
;
A52:
for
w being
object st
w in dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) holds
h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w
dom h2 = dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1}))
by A39, A37, A50, PARTFUN1:def 2;
hence
z in Z
by A37, A41, A52, CARD_3:def 5;
verum
end;
hence
z in X9
by A10, A12, A22, A35, SETFAM_1:43;
verum
end;
A54:
X9 c= uparrow y
proof
set h1 =
chi (
x,
I);
let z be
object ;
TARSKI:def 3 ( not z in X9 or z in uparrow y )
assume A55:
z in X9
;
z in uparrow y
then reconsider z9 =
z as
Element of
(product (I --> (BoolePoset {0}))) by A10, A12;
z in the
carrier of
(product (I --> (BoolePoset {0})))
by A10, A12, A55;
then
z in product (Carrier (I --> (BoolePoset {0})))
by YELLOW_1:def 4;
then consider h2 being
Function such that A56:
z = h2
and
dom h2 = dom (Carrier (I --> (BoolePoset {0})))
and A57:
for
w being
object st
w in dom (Carrier (I --> (BoolePoset {0}))) holds
h2 . w in (Carrier (I --> (BoolePoset {0}))) . w
by CARD_3:def 5;
A58:
for
i being
object st
i in I holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = (I --> (BoolePoset {0})) . i &
xi = (chi (x,I)) . i &
yi = h2 . i &
xi <= yi )
proof
let i be
object ;
( i in I implies ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi ) )
assume A59:
i in I
;
ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
then reconsider i9 =
i as
Element of
I ;
ex
RB being
1-sorted st
(
RB = (I --> (BoolePoset {0})) . i &
(Carrier (I --> (BoolePoset {0}))) . i = the
carrier of
RB )
by A59, PRALG_1:def 15;
then A60:
(Carrier (I --> (BoolePoset {0}))) . i = {0,1}
by A2, A59, FUNCOP_1:7;
take RS =
BoolePoset {0};
ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
A61:
i in dom (Carrier (I --> (BoolePoset {0})))
by A59, PARTFUN1:def 2;
then A62:
h2 . i in (Carrier (I --> (BoolePoset {0}))) . i
by A57;
per cases
( i in x or not i in x )
;
suppose A63:
i in x
;
ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )reconsider xi = 1,
yi = 1 as
Element of
RS by A2, TARSKI:def 2;
take
xi
;
ex yi being Element of RS st
( RS = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )take
yi
;
( RS = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )thus
RS = (I --> (BoolePoset {0})) . i
by A59, FUNCOP_1:7;
( xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )thus
xi = (chi (x,I)) . i
by A63, FUNCT_3:def 3;
( yi = h2 . i & xi <= yi )A64:
((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) . i9 = {1}
by A9, A61, FUNCT_7:31;
product ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) in ZZ
by A33, A63;
then
z in product ((Carrier (I --> Sierpinski_Space)) +* (i9,{1}))
by A22, A55, SETFAM_1:43;
then consider h29 being
Function such that A65:
z = h29
and
dom h29 = dom ((Carrier (I --> Sierpinski_Space)) +* (i9,{1}))
and A66:
for
w being
object st
w in dom ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) holds
h29 . w in ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) . w
by CARD_3:def 5;
i9 in dom ((Carrier (I --> Sierpinski_Space)) +* (i9,{1}))
by A9, A61, FUNCT_7:30;
then
h29 . i9 in ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) . i9
by A66;
hence
yi = h2 . i
by A56, A65, A64, TARSKI:def 1;
xi <= yithus
xi <= yi
;
verum end; end;
end;
chi (
x,
I)
= y
by A14;
then
y <= z9
by A1, A56, A58, YELLOW_1:def 4;
hence
z in uparrow y
by WAYBEL_0:18;
verum
end;
reconsider Y =
y as
Element of
T9 by A10;
x is
compact
by A25, WAYBEL_8:28;
then
y is
compact
by A13, WAYBEL13:28;
then
Y is
compact
by A10, WAYBEL_8:9;
then A70:
Y in the
carrier of
(CompactSublatt T9)
by WAYBEL_8:def 1;
uparrow Y =
uparrow {Y}
by WAYBEL_0:def 18
.=
uparrow {y}
by A10, WAYBEL_0:13
.=
uparrow y
by WAYBEL_0:def 18
;
then
X = uparrow Y
by A54, A34, XBOOLE_0:def 10;
hence
X in R
by A11, A70;
verum
end;
A71:
rng f = the carrier of (product (I --> (BoolePoset {0})))
by A13, WAYBEL_0:66;
R c= FinMeetCl P
proof
deffunc H1(
Element of
I)
-> set =
product ((Carrier (I --> Sierpinski_Space)) +* ($1,{1}));
let X be
object ;
TARSKI:def 3 ( not X in R or X in FinMeetCl P )
assume A72:
X in R
;
X in FinMeetCl P
then consider Y being
Element of
T9 such that A73:
X = uparrow Y
and A74:
Y in the
carrier of
(CompactSublatt T9)
by A11;
reconsider X9 =
X as
Subset of
(product (I --> Sierpinski_Space)) by A12, A72;
reconsider y =
Y as
Element of
(product (I --> (BoolePoset {0}))) by A10;
consider x being
object such that A75:
x in dom f
and A76:
y = f . x
by A71, FUNCT_1:def 3;
reconsider x =
x as
Element of
(BoolePoset I) by A75;
Y is
compact
by A74, WAYBEL_8:def 1;
then
y is
compact
by A10, WAYBEL_8:9;
then
x is
compact
by A13, A76, WAYBEL13:28;
then A77:
x is
finite
by WAYBEL_8:28;
A78:
{ H1(jj) where jj is Element of I : jj in x } is
finite
from FRAENKEL:sch 21(A77);
set ZZ =
{ (product ((Carrier (I --> Sierpinski_Space)) +* (jj,{1}))) where jj is Element of I : jj in x } ;
reconsider x9 =
x as
Subset of
I by WAYBEL_8:26;
A79:
{ (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;
A80:
uparrow Y =
uparrow {Y}
by WAYBEL_0:def 18
.=
uparrow {y}
by A10, WAYBEL_0:13
.=
uparrow y
by WAYBEL_0:def 18
;
A81:
Intersect ZZ c= X9
proof
set h1 =
chi (
x,
I);
let z be
object ;
TARSKI:def 3 ( not z in Intersect ZZ or z in X9 )
assume A82:
z in Intersect ZZ
;
z in X9
then reconsider z9 =
z as
Element of
(product (I --> (BoolePoset {0}))) by A10, A12;
z in the
carrier of
(product (I --> (BoolePoset {0})))
by A10, A12, A82;
then
z in product (Carrier (I --> (BoolePoset {0})))
by YELLOW_1:def 4;
then consider h2 being
Function such that A83:
z = h2
and
dom h2 = dom (Carrier (I --> (BoolePoset {0})))
and A84:
for
w being
object st
w in dom (Carrier (I --> (BoolePoset {0}))) holds
h2 . w in (Carrier (I --> (BoolePoset {0}))) . w
by CARD_3:def 5;
A85:
for
i being
object st
i in I holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = (I --> (BoolePoset {0})) . i &
xi = (chi (x,I)) . i &
yi = h2 . i &
xi <= yi )
proof
let i be
object ;
( i in I implies ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi ) )
assume A86:
i in I
;
ex R being RelStr ex xi, yi being Element of R st
( R = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
then reconsider i9 =
i as
Element of
I ;
ex
RB being
1-sorted st
(
RB = (I --> (BoolePoset {0})) . i &
(Carrier (I --> (BoolePoset {0}))) . i = the
carrier of
RB )
by A86, PRALG_1:def 15;
then A87:
(Carrier (I --> (BoolePoset {0}))) . i = {0,1}
by A2, A86, FUNCOP_1:7;
take RS =
BoolePoset {0};
ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )
A88:
i in dom (Carrier (I --> (BoolePoset {0})))
by A86, PARTFUN1:def 2;
then A89:
h2 . i in (Carrier (I --> (BoolePoset {0}))) . i
by A84;
per cases
( i in x or not i in x )
;
suppose A90:
i in x
;
ex xi, yi being Element of RS st
( RS = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )reconsider xi = 1,
yi = 1 as
Element of
RS by A2, TARSKI:def 2;
take
xi
;
ex yi being Element of RS st
( RS = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )take
yi
;
( RS = (I --> (BoolePoset {0})) . i & xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )thus
RS = (I --> (BoolePoset {0})) . i
by A86, FUNCOP_1:7;
( xi = (chi (x,I)) . i & yi = h2 . i & xi <= yi )thus
xi = (chi (x,I)) . i
by A86, A90, FUNCT_3:def 3;
( yi = h2 . i & xi <= yi )A91:
((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) . i9 = {1}
by A9, A88, FUNCT_7:31;
product ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) in ZZ
by A90;
then
z in product ((Carrier (I --> Sierpinski_Space)) +* (i9,{1}))
by A82, SETFAM_1:43;
then consider h29 being
Function such that A92:
z = h29
and
dom h29 = dom ((Carrier (I --> Sierpinski_Space)) +* (i9,{1}))
and A93:
for
w being
object st
w in dom ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) holds
h29 . w in ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) . w
by CARD_3:def 5;
i9 in dom ((Carrier (I --> Sierpinski_Space)) +* (i9,{1}))
by A9, A88, FUNCT_7:30;
then
h29 . i9 in ((Carrier (I --> Sierpinski_Space)) +* (i9,{1})) . i9
by A93;
hence
yi = h2 . i
by A83, A92, A91, TARSKI:def 1;
xi <= yithus
xi <= yi
;
verum end; end;
end;
chi (
x,
I) =
f . x9
by A14
.=
y
by A76
;
then
y <= z9
by A1, A83, A85, YELLOW_1:def 4;
hence
z in X9
by A73, A80, WAYBEL_0:18;
verum
end;
X9 c= Intersect ZZ
proof
let z be
object ;
TARSKI:def 3 ( not z in X9 or z in Intersect ZZ )
assume A97:
z in X9
;
z in Intersect ZZ
then reconsider z9 =
z as
Element of
(product (I --> (BoolePoset {0}))) by A10, A12;
y <= z9
by A73, A80, A97, WAYBEL_0:18;
then consider h1,
h2 being
Function such that A98:
h1 = y
and A99:
h2 = z9
and A100:
for
i being
object st
i in I holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = (I --> (BoolePoset {0})) . i &
xi = h1 . i &
yi = h2 . i &
xi <= yi )
by A1, YELLOW_1:def 4;
z in the
carrier of
(product (I --> (BoolePoset {0})))
by A10, A12, A97;
then
z in product (Carrier (I --> (BoolePoset {0})))
by YELLOW_1:def 4;
then A101:
ex
gg being
Function st
(
z = gg &
dom gg = dom (Carrier (I --> (BoolePoset {0}))) & ( for
w being
object st
w in dom (Carrier (I --> (BoolePoset {0}))) holds
gg . w in (Carrier (I --> (BoolePoset {0}))) . w ) )
by CARD_3:def 5;
A102:
h1 =
f . x9
by A76, A98
.=
chi (
x,
I)
by A14
;
for
Z being
set st
Z in ZZ holds
z in Z
proof
let Z be
set ;
( Z in ZZ implies z in Z )
assume
Z in ZZ
;
z in Z
then consider j being
Element of
I such that A103:
Z = product ((Carrier (I --> Sierpinski_Space)) +* (j,{1}))
and A104:
j in x
;
consider RS being
RelStr ,
xj,
yj being
Element of
RS such that A105:
RS = (I --> (BoolePoset {0})) . j
and A106:
xj = h1 . j
and A107:
yj = h2 . j
and A108:
xj <= yj
by A100;
reconsider a =
xj,
b =
yj as
Element of
(BoolePoset {0}) by A105;
A109:
a <= b
by A105, A108;
A110:
xj = 1
by A102, A104, A106, FUNCT_3:def 3;
A111:
yj <> 0
A112:
dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) =
dom (Carrier (I --> Sierpinski_Space))
by FUNCT_7:30
.=
I
by PARTFUN1:def 2
;
A113:
b in the
carrier of
(BoolePoset {0})
;
A114:
for
w being
object st
w in dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) holds
h2 . w in ((Carrier (I --> Sierpinski_Space)) +* (j,{1})) . w
dom h2 = dom ((Carrier (I --> Sierpinski_Space)) +* (j,{1}))
by A101, A99, A112, PARTFUN1:def 2;
hence
z in Z
by A99, A103, A114, CARD_3:def 5;
verum
end;
hence
z in Intersect ZZ
by A97, SETFAM_1:43;
verum
end;
then
X9 = Intersect ZZ
by A81;
hence
X in FinMeetCl P
by A79, A78, CANTOR_1:def 3;
verum
end;
then
R = FinMeetCl P
by A16;
then
P9 is prebasis of T
by A12, YELLOW_9:23;
hence
the topology of T = the topology of (product (I --> Sierpinski_Space))
by A12, YELLOW_9:26; verum