Copyright (c) 2000 Association of Mizar Users
environ
vocabulary ORDERS_1, SETFAM_1, WAYBEL_0, TARSKI, LATTICES, ORDINAL2, WAYBEL23,
YELLOW_1, YELLOW_0, WAYBEL_8, CARD_1, ORDINAL1, SUBSET_1, PRE_TOPC,
CANTOR_1, WAYBEL_3, BOOLE, FINSET_1, TSP_1, FUNCT_1, RELAT_1, WAYBEL11,
YELLOW_9, WAYBEL19, PRELAMB, DIRAF, PROB_1, COMPTS_1, QUANTAL1, LATTICE3,
REALSET1, RELAT_2, FILTER_2, FINSEQ_1, MATRIX_2, BHSP_3, FINSEQ_4,
WAYBEL_9, WELLORD1, CAT_1, WAYBEL31, RLVECT_3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, STRUCT_0, FINSET_1,
RELSET_1, GROUP_1, RELAT_1, REALSET1, FUNCT_1, FUNCT_2, FINSEQ_1,
FINSEQ_2, FINSEQ_4, MATRIX_2, ORDINAL1, CARD_1, PRE_TOPC, TSP_1, TOPS_2,
CANTOR_1, ORDERS_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_9,
WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_8, WAYBEL_9, WAYBEL11, WAYBEL19,
WAYBEL23;
constructors NAT_1, GROUP_1, FINSEQ_4, MATRIX_2, TSP_1, TOPS_2, CANTOR_1,
URYSOHN1, ORDERS_3, YELLOW_9, WAYBEL_1, WAYBEL_8, WAYBEL11, WAYBEL19,
WAYBEL23, MEMBERED;
clusters STRUCT_0, RELSET_1, FINSET_1, FINSEQ_1, CARD_1, TSP_1, SUBSET_1,
CANTOR_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_9,
YELLOW11, YELLOW13, YELLOW15, WAYBEL_0, WAYBEL_3, WAYBEL_4, WAYBEL_8,
WAYBEL14, WAYBEL19, WAYBEL23, WAYBEL25, WAYBEL30, ZFMISC_1;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, YELLOW_0, WAYBEL_8;
theorems TARSKI, SETFAM_1, SUBSET_1, FINSET_1, RELSET_1, FUNCT_1, FUNCT_2,
FINSEQ_1, FINSEQ_5, MATRLIN, CARD_1, CARD_2, CARD_4, WELLORD2, T_0TOPSP,
ORDERS_1, GROUP_1, PRE_TOPC, TOPS_1, TOPS_2, CANTOR_1, LATTICE3,
YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_8, YELLOW_9, YELLOW12, YELLOW15,
WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_4, WAYBEL_7, WAYBEL_8, WAYBEL11,
WAYBEL14, WAYBEL19, WAYBEL23, WAYBEL30, WAYBEL13, WSIERP_1, XBOOLE_0,
XBOOLE_1, TRIANG_1;
schemes ORDINAL1, FUNCT_2, PRE_CIRC, ZFREFLE1, FRAENKEL, COMPTS_1;
begin
scheme UparrowUnion{L1()->RelStr,P[set]}:
for S be Subset-Family of L1() st
S = { X where X is Subset of L1() : P[X] } holds
uparrow union S = union { uparrow X where X is Subset of L1() : P[X] }
proof
let S be Subset-Family of L1();
assume A1: S = { X where X is Subset of L1() : P[X] };
A2: uparrow union S c= union { uparrow X where X is Subset of L1() : P[X]}
proof
let z be set;
assume A3: z in uparrow union S;
then reconsider z1 = z as Element of L1();
consider y1 be Element of L1() such that
A4: y1 <= z1 and
A5: y1 in union S by A3,WAYBEL_0:def 16;
consider Z be set such that
A6: y1 in Z and
A7: Z in S by A5,TARSKI:def 4;
consider X1 be Subset of L1() such that
A8: Z = X1 and
A9: P[X1] by A1,A7;
A10: z in uparrow X1 by A4,A6,A8,WAYBEL_0:def 16;
uparrow X1 in { uparrow X where X is Subset of L1() : P[X] } by A9;
hence z in union { uparrow X where X is Subset of L1() : P[X] }
by A10,TARSKI:def 4;
end;
union { uparrow X where X is Subset of L1() : P[X] } c= uparrow union S
proof
let z be set;
assume z in union { uparrow X where X is Subset of L1() : P[X] };
then consider Z be set such that
A11: z in Z and
A12: Z in
{ uparrow X where X is Subset of L1() : P[X] } by TARSKI:def 4;
consider X1 be Subset of L1() such that
A13: Z = uparrow X1 and
A14: P[X1] by A12;
reconsider z1 = z as Element of L1() by A11,A13;
consider y1 be Element of L1() such that
A15: y1 <= z1 and
A16: y1 in X1 by A11,A13,WAYBEL_0:def 16;
X1 in S by A1,A14;
then y1 in union S by A16,TARSKI:def 4;
hence z in uparrow union S by A15,WAYBEL_0:def 16;
end;
hence uparrow union S =
union { uparrow X where X is Subset of L1() : P[X] } by A2,XBOOLE_0:def 10
;
end;
scheme DownarrowUnion{L1()->RelStr,P[set]}:
for S be Subset-Family of L1() st
S = { X where X is Subset of L1() : P[X] } holds
downarrow union S = union { downarrow X where X is Subset of L1() : P[X]}
proof
let S be Subset-Family of L1();
assume A1: S = { X where X is Subset of L1() : P[X] };
A2: downarrow union S c=
union { downarrow X where X is Subset of L1() : P[X] }
proof
let z be set;
assume A3: z in downarrow union S;
then reconsider z1 = z as Element of L1();
consider y1 be Element of L1() such that
A4: y1 >= z1 and
A5: y1 in union S by A3,WAYBEL_0:def 15;
consider Z be set such that
A6: y1 in Z and
A7: Z in S by A5,TARSKI:def 4;
consider X1 be Subset of L1() such that
A8: Z = X1 and
A9: P[X1] by A1,A7;
A10: z in downarrow X1 by A4,A6,A8,WAYBEL_0:def 15;
downarrow X1 in { downarrow X where X is Subset of L1() : P[X] } by A9;
hence z in union { downarrow X where X is Subset of L1() : P[X] }
by A10,TARSKI:def 4;
end;
union { downarrow X where X is Subset of L1(): P[X] } c= downarrow union
S
proof
let z be set;
assume z in union { downarrow X where X is Subset of L1() : P[X] };
then consider Z be set such that
A11: z in Z and
A12: Z in
{ downarrow X where X is Subset of L1(): P[X]} by TARSKI:def 4;
consider X1 be Subset of L1() such that
A13: Z = downarrow X1 and
A14: P[X1] by A12;
reconsider z1 = z as Element of L1() by A11,A13;
consider y1 be Element of L1() such that
A15: y1 >= z1 and
A16: y1 in X1 by A11,A13,WAYBEL_0:def 15;
X1 in S by A1,A14;
then y1 in union S by A16,TARSKI:def 4;
hence z in downarrow union S by A15,WAYBEL_0:def 15;
end;
hence downarrow union S = union { downarrow X where X is Subset of L1() :
P[X] } by A2,XBOOLE_0:def 10;
end;
definition
let L1 be lower-bounded continuous sup-Semilattice;
let B1 be with_bottom CLbasis of L1;
cluster InclPoset Ids subrelstr B1 -> algebraic;
coherence by WAYBEL13:10;
end;
definition :: DEFINITION 4.5
let L1 be continuous sup-Semilattice;
func CLweight L1 -> Cardinal equals :Def1:
meet {Card B1 where B1 is with_bottom CLbasis of L1 : not contradiction};
coherence
proof
defpred P[Ordinal] means
$1 in {Card B1 where B1 is with_bottom CLbasis of L1 : not contradiction};
A1: ex A be Ordinal st P[A]
proof
take Card [#]L1;
[#]L1 is CLbasis of L1 by YELLOW15:26;
hence thesis;
end;
consider A be Ordinal such that
A2: P[A] and
A3: for C be Ordinal st P[C] holds A c= C from Ordinal_Min(A1);
consider B1 be with_bottom CLbasis of L1 such that
A4: A = Card B1 by A2;
reconsider A as Cardinal by A4;
set X = { Card B2 where B2 is with_bottom CLbasis of L1 :
not contradiction };
[#]L1 is CLbasis of L1 by YELLOW15:26;
then A5: Card [#]L1 in X;
now let x be set;
thus (for y be set holds y in X implies x in y) implies x in A by A2;
assume A6: x in A;
let y be set;
assume A7: y in X;
then consider B2 be with_bottom CLbasis of L1 such that
A8: y = Card B2;
reconsider y1 = y as Cardinal by A8;
A c= y1 by A3,A7;
hence x in y by A6;
end;
hence thesis by A5,SETFAM_1:def 1;
end;
end;
theorem Th1:
for T be TopStruct
for b be Basis of T holds
weight T c= Card b
proof
let T be TopStruct;
let b be Basis of T;
Card b in { Card B1 where B1 is Basis of T : not contradiction };
then meet { Card B1 where B1 is Basis of T : not contradiction } c= Card b
by SETFAM_1:4;
hence weight T c= Card b by WAYBEL23:def 5;
end;
theorem Th2:
for T be TopStruct
ex b be Basis of T st
Card b = weight T
proof
let T be TopStruct;
defpred P[Ordinal] means
$1 in { Card b where b is Basis of T : not contradiction };
A1: ex A be Ordinal st P[A]
proof
take Card the topology of T;
the topology of T is Basis of T by CANTOR_1:2;
hence thesis;
end;
consider A be Ordinal such that
A2: P[A] and
A3: for C be Ordinal st P[C] holds A c= C from Ordinal_Min(A1);
consider b be Basis of T such that
A4: A = Card b by A2;
take b;
set X = { Card b1 where b1 is Basis of T : not contradiction };
the topology of T is Basis of T by CANTOR_1:2;
then A5: Card the topology of T in X;
now let x be set;
thus (for y be set holds y in X implies x in y) implies x in A by A2;
assume A6: x in A;
let y be set;
assume A7: y in X;
then consider B2 be Basis of T such that
A8: y = Card B2;
reconsider y1 = y as Cardinal by A8;
A c= y1 by A3,A7;
hence x in y by A6;
end;
hence Card b = meet X by A4,A5,SETFAM_1:def 1
.= weight T by WAYBEL23:def 5;
end;
theorem Th3:
for L1 be continuous sup-Semilattice
for B1 be with_bottom CLbasis of L1 holds
CLweight L1 c= Card B1
proof
let L1 be continuous sup-Semilattice;
let B1 be with_bottom CLbasis of L1;
Card B1 in { Card B2 where B2 is with_bottom CLbasis of L1 :
not contradiction };
then meet { Card B2 where B2 is with_bottom CLbasis of L1 :
not contradiction } c= Card B1 by SETFAM_1:4;
hence CLweight L1 c= Card B1 by Def1;
end;
theorem Th4:
for L1 be continuous sup-Semilattice
ex B1 be with_bottom CLbasis of L1 st
Card B1 = CLweight L1
proof
let L1 be continuous sup-Semilattice;
defpred P[Ordinal] means
$1 in {Card B1 where B1 is with_bottom CLbasis of L1 : not contradiction};
A1: ex A be Ordinal st P[A]
proof
take Card [#]L1;
[#]L1 is CLbasis of L1 by YELLOW15:26;
hence thesis;
end;
consider A be Ordinal such that
A2:P[A] and
A3: for C be Ordinal st P[C] holds A c= C from Ordinal_Min(A1);
consider B1 be with_bottom CLbasis of L1 such that
A4: A = Card B1 by A2;
take B1;
set X = { Card B2 where B2 is with_bottom CLbasis of L1 :
not contradiction };
[#]L1 is CLbasis of L1 by YELLOW15:26;
then A5: Card [#]L1 in X;
now let x be set;
thus (for y be set holds y in X implies x in y) implies x in A by A2;
assume A6: x in A;
let y be set;
assume A7: y in X;
then consider B2 be with_bottom CLbasis of L1 such that
A8: y = Card B2;
reconsider y1 = y as Cardinal by A8;
A c= y1 by A3,A7;
hence x in y by A6;
end;
hence Card B1 = meet X by A4,A5,SETFAM_1:def 1
.= CLweight L1 by Def1;
end;
theorem Th5: :: Under 4.5.
for L1 be algebraic lower-bounded LATTICE holds
CLweight L1 = Card the carrier of CompactSublatt L1
proof
let L1 be algebraic lower-bounded LATTICE;
set CB = {Card B1 where B1 is with_bottom CLbasis of L1 :
not contradiction};
the carrier of CompactSublatt L1 is with_bottom CLbasis of L1
by WAYBEL23:72;
then A1: Card the carrier of CompactSublatt L1 in CB;
then A2: meet CB c= Card the carrier of CompactSublatt L1 by SETFAM_1:4;
now let X be set;
assume X in CB;
then consider B1 be with_bottom CLbasis of L1 such that
A3: X = Card B1;
the carrier of CompactSublatt L1 c= B1 by WAYBEL23:72;
hence Card the carrier of CompactSublatt L1 c= X by A3,CARD_1:27;
end;
then Card the carrier of CompactSublatt L1 c= meet CB by A1,SETFAM_1:6;
then meet CB = Card the carrier of CompactSublatt L1 by A2,XBOOLE_0:def 10
;
hence CLweight L1 = Card the carrier of CompactSublatt L1 by Def1;
end;
theorem Th6:
for T be non empty TopSpace
for L1 be continuous sup-Semilattice st
InclPoset the topology of T = L1
for B1 be with_bottom CLbasis of L1 holds
B1 is Basis of T
proof
let T be non empty TopSpace;
let L1 be continuous sup-Semilattice;
assume A1: InclPoset the topology of T = L1;
let B1 be with_bottom CLbasis of L1;
B1 c= the carrier of L1;
then B1 c= the topology of T by A1,YELLOW_1:1;
then B1 c= bool the carrier of T by XBOOLE_1:1;
then B1 is Subset-Family of T by SETFAM_1:def 7;
then reconsider B2 = B1 as Subset-Family of T;
A2: B2 c= the topology of T
proof
let x be set;
assume x in B2;
then reconsider x1 = x as Element of L1;
x1 in the carrier of L1;
hence x in the topology of T by A1,YELLOW_1:1;
end;
for A be Subset of T st A is open
for p be Point of T st p in A
ex a be Subset of T st a in B2 & p in a & a c= A
proof
let A be Subset of T;
assume A3: A is open;
let p be Point of T;
assume A4: p in A;
A in the topology of T by A3,PRE_TOPC:def 5;
then A in the carrier of L1 by A1,YELLOW_1:1;
then reconsider A1 = A as Element of L1;
A1 = sup (waybelow A1 /\ B1) by WAYBEL23:def 7
.= union (waybelow A1 /\ B1) by A1,YELLOW_1:22;
then consider a be set such that
A5: p in a and
A6: a in waybelow A1 /\ B1 by A4,TARSKI:def 4;
a in the carrier of L1 by A6;
then a in the topology of T by A1,YELLOW_1:1;
then reconsider a as Subset of T;
take a;
thus a in B2 by A6,XBOOLE_0:def 3;
thus p in a by A5;
reconsider a1 = a as Element of L1 by A6;
a1 in waybelow A1 by A6,XBOOLE_0:def 3;
then a1 << A1 by WAYBEL_3:7;
then a1 <= A1 by WAYBEL_3:1;
hence a c= A by A1,YELLOW_1:3;
end;
hence B1 is Basis of T by A2,YELLOW_9:32;
end;
theorem Th7:
for T be non empty TopSpace
for L1 be continuous lower-bounded LATTICE st
InclPoset the topology of T = L1
for B1 be Basis of T
for B2 be Subset of L1 st B1 = B2 holds
finsups B2 is with_bottom CLbasis of L1
proof
let T be non empty TopSpace;
let L1 be continuous lower-bounded LATTICE;
assume A1: InclPoset the topology of T = L1;
let B1 be Basis of T;
let B2 be Subset of L1;
assume A2: B1 = B2;
now let x,y be Element of L1;
assume that
A3: x in finsups B2 and
A4: y in finsups B2;
x in { "\/"(Y,L1) where Y is finite Subset of B2: ex_sup_of Y,L1 }
by A3,WAYBEL_0:def 27;
then consider Y1 be finite Subset of B2 such that
A5: x = "\/"(Y1,L1) and
A6: ex_sup_of Y1,L1;
y in { "\/"(Y,L1) where Y is finite Subset of B2: ex_sup_of Y,L1 }
by A4,WAYBEL_0:def 27;
then consider Y2 be finite Subset of B2 such that
A7: y = "\/"(Y2,L1) and
A8: ex_sup_of Y2,L1;
ex_sup_of (Y1 \/ Y2),L1 & "\/"(Y1 \/ Y2, L1) = "\/"(Y1, L1) "\/" "\/"
(Y2, L1)
by A6,A8,YELLOW_2:3;
then x "\/" y in { "\/"
(Y,L1) where Y is finite Subset of B2: ex_sup_of Y,L1 }
by A5,A7;
then x "\/" y in finsups B2 by WAYBEL_0:def 27;
hence sup {x,y} in finsups B2 by YELLOW_0:41;
end;
then A9: finsups B2 is join-closed by WAYBEL23:18;
{} c= B2 & ex_sup_of {},L1 by XBOOLE_1:2,YELLOW_0:42;
then "\/"({},L1) in
{"\/"(Y,L1) where Y is finite Subset of B2: ex_sup_of Y,L1};
then "\/"({},L1) in finsups B2 by WAYBEL_0:def 27;
then A10: Bottom L1 in finsups B2 by YELLOW_0:def 11;
for x,y be Element of L1 st not y <= x
ex b be Element of L1 st b in finsups B2 & not b <= x & b <= y
proof
let x,y be Element of L1;
x in the carrier of L1 & y in the carrier of L1;
then A11: x in the topology of T & y in
the topology of T by A1,YELLOW_1:1;
then reconsider y1 = y as Subset of T;
assume not y <= x;
then not y c= x by A1,YELLOW_1:3;
then consider v be set such that
A12: v in y and
A13: not v in x by TARSKI:def 3;
v in y1 by A12;
then reconsider v as Point of T;
y1 is open by A11,PRE_TOPC:def 5;
then consider b be Subset of T such that
A14: b in B1 and
A15: v in b and
A16: b c= y1 by A12,YELLOW_9:31;
reconsider b as Element of L1 by A2,A14;
take b;
for z be set st z in {b} holds z in B2 by A2,A14,TARSKI:def 1;
then A17: {b} is finite Subset of B2 by TARSKI:def 3;
A18: ex_sup_of {b},L1 by YELLOW_0:38;
b = "\/"({b},L1) by YELLOW_0:39;
then b in { "\/"(Y,L1) where Y is finite Subset of B2: ex_sup_of Y,L1 }
by A17,A18;
hence b in finsups B2 by WAYBEL_0:def 27;
not b c= x by A13,A15;
hence not b <= x by A1,YELLOW_1:3;
thus b <= y by A1,A16,YELLOW_1:3;
end;
hence finsups B2 is with_bottom CLbasis of L1
by A9,A10,WAYBEL23:49,def 8;
end;
theorem Th8: :: PROPOSITION 4.6 (i)
for T be T_0 non empty TopSpace
for L1 be continuous lower-bounded sup-Semilattice st
InclPoset the topology of T = L1 holds
T is infinite implies weight T = CLweight L1
proof
let T be T_0 non empty TopSpace;
let L1 be continuous lower-bounded sup-Semilattice;
assume that
A1: InclPoset the topology of T = L1 and
A2: T is infinite;
A3: { Card B1 where B1 is Basis of T : not contradiction } c=
{ Card B1 where B1 is with_bottom CLbasis of L1 : not contradiction }
proof
let b be set;
assume b in { Card B1 where B1 is Basis of T : not contradiction };
then consider B2 be Basis of T such that
A4: b = Card B2;
B2 c= the topology of T by CANTOR_1:def 2;
then B2 c= the carrier of L1 by A1,YELLOW_1:1;
then reconsider B3 = B2 as Subset of L1;
B2 is infinite by A2,YELLOW15:31;
then A5: Card B2 = Card finsups B3 by YELLOW15:28;
finsups B3 is with_bottom CLbasis of L1 by A1,Th7;
hence b in { Card B1 where B1 is with_bottom CLbasis of L1 :
not contradiction } by A4,A5;
end;
{ Card B1 where B1 is with_bottom CLbasis of L1 : not contradiction } c=
{ Card B1 where B1 is Basis of T : not contradiction }
proof
let b be set;
assume b in { Card B1 where B1 is with_bottom CLbasis of L1 :
not contradiction };
then consider B2 be with_bottom CLbasis of L1 such that
A6: b = Card B2;
B2 is Basis of T by A1,Th6;
hence b in { Card B1 where B1 is Basis of T : not contradiction } by A6;
end;
then { Card B1 where B1 is Basis of T : not contradiction } =
{ Card B1 where B1 is with_bottom CLbasis of L1 : not contradiction }
by A3,XBOOLE_0:def 10
;
hence weight T = meet { Card B1 where B1 is with_bottom CLbasis of L1 :
not contradiction } by WAYBEL23:def 5
.= CLweight L1 by Def1;
end;
theorem Th9: :: PROPOSITION 4.6 (ii) (a)
for T be T_0 non empty TopSpace
for L1 be continuous sup-Semilattice st
InclPoset the topology of T = L1 holds
Card the carrier of T c= Card the carrier of L1
proof
let T be T_0 non empty TopSpace;
let L1 be continuous sup-Semilattice;
assume A1: InclPoset the topology of T = L1;
Card the carrier of T c= Card the topology of T by YELLOW15:29;
hence Card the carrier of T c= Card the carrier of L1 by A1,YELLOW_1:1;
end;
theorem Th10: :: PROPOSITION 4.6 (ii) (b)
for T be T_0 non empty TopSpace st T is finite holds
weight T = Card the carrier of T
proof
let T be T_0 non empty TopSpace;
assume A1: T is finite;
deffunc F(set) =
meet { A where A is Element of the topology of T : $1 in A };
A2: for x be set st x in the carrier of T holds
F(x) in the carrier of BoolePoset the carrier of T
proof
let x be set;
A3: the carrier of T in the topology of T by PRE_TOPC:def 1;
assume x in the carrier of T;
then the carrier of T in
{ A where A is Element of the topology of T : x in A } by A3;
then meet { A where A is Element of the topology of T : x in A } c=
the carrier of T by SETFAM_1:4;
then meet { A where A is Element of the topology of T : x in A } in
bool the carrier of T;
hence meet { A where A is Element of the topology of T : x in A } in
the carrier of BoolePoset the carrier of T by WAYBEL_7:4;
end;
consider f be Function of the carrier of T,
the carrier of BoolePoset the carrier of T
such that
A4: for x be set st x in the carrier of T holds f.x = F(x)
from Lambda1(A2);
rng f c= the carrier of BoolePoset the carrier of T;
then rng f c= bool the carrier of T by WAYBEL_7:4;
then rng f is Subset-Family of T by SETFAM_1:def 7;
then reconsider rf = rng f as Subset-Family of T;
A5: rf c= the topology of T
proof
let z be set;
assume z in rf;
then consider y be set such that
A6: y in dom f and
A7: z = f.y by FUNCT_1:def 5;
y in the carrier of T by A6,FUNCT_2:def 1;
then A8: z = meet { A where A is Element of the topology of T : y in A }
by A4,A7;
{ A where A is Element of the topology of T : y in A } c=
bool the carrier of T
proof
let z be set;
assume z in { A where A is Element of the topology of T : y in A };
then consider A be Element of the topology of T such that
A9: z = A and
y in A;
thus z in bool the carrier of T by A9;
end;
then reconsider sfA = { A where A is Element of the topology of T :
y in A } as Subset-Family of T by SETFAM_1:def 7;
reconsider sfA as Subset-Family of T;
now let P be Subset of T;
assume P in sfA;
then consider A be Element of the topology of T such that
A10: P = A and
y in A;
thus P is open by A10,PRE_TOPC:def 5;
end;
then A11: sfA is open by TOPS_2:def 1;
the carrier of T is finite by A1,GROUP_1:def 13;
then reconsider tT = the topology of T as finite non empty set
by YELLOW15:3;
deffunc F(set) = $1;
defpred P[set] means y in $1;
{F(A) where A is Element of tT: P[A]} is finite from FraenkelFinIm;
then meet sfA is open by A11,TOPS_2:27;
hence z in the topology of T by A8,PRE_TOPC:def 5;
end;
for A be Subset of T st A is open
for p be Point of T st p in A
ex a be Subset of T st a in rf & p in a & a c= A
proof
let A be Subset of T;
assume A12: A is open;
let p be Point of T;
assume A13: p in A;
A in the topology of T by A12,PRE_TOPC:def 5;
then A14: A in { C where C is Element of the topology of T : p in
C } by A13
;
meet { C where C is Element of the topology of T : p in C } c=
the carrier of T
proof
let z be set;
assume z in meet { C where C is Element of the topology of T :
p in C };
then z in A by A14,SETFAM_1:def 1;
hence z in the carrier of T;
end;
then reconsider a = meet { C where C is Element of the topology of T :
p in C } as Subset of T;
take a;
p in the carrier of T;
then A15: p in dom f by FUNCT_2:def 1;
a = f.p by A4;
hence a in rf by A15,FUNCT_1:def 5;
now let Y be set;
assume Y in { C where C is Element of the topology of T : p in C };
then consider C be Element of the topology of T such that
A16: Y = C and
A17: p in C;
thus p in Y by A16,A17;
end;
hence p in a by A14,SETFAM_1:def 1;
thus a c= A
proof
let z be set;
assume z in a;
hence z in A by A14,SETFAM_1:def 1;
end;
end;
then rng f is Basis of T by A5,YELLOW_9:32;
then A18: Card rng f in {Card B1 where B1 is Basis of T : not contradiction
};
then A19: meet { Card B1 where B1 is Basis of T : not contradiction } c=
Card rng f by SETFAM_1:4;
for X be set st X in { Card B1 where B1 is Basis of T : not contradiction
}
holds Card rng f c= X
proof
let X be set;
assume X in { Card B1 where B1 is Basis of T : not contradiction };
then consider B2 be Basis of T such that
A20: X = Card B2;
rng f c= B2
proof
let y be set;
assume y in rng f;
then consider x be set such that
A21: x in dom f and
A22: y = f.x by FUNCT_1:def 5;
x in the carrier of T by A21,FUNCT_2:def 1;
then reconsider x1 = x as Element of T;
y = meet{ A where A is Element of the topology of T : x1 in
A } by A4,A22;
hence y in B2 by A1,YELLOW15:32;
end;
hence Card rng f c= X by A20,CARD_1:27;
end;
then Card rng f c= meet { Card B1 where B1 is Basis of T :
not contradiction } by A18,SETFAM_1:6;
then A23: Card rng f = meet { Card B1 where B1 is Basis of T :
not contradiction } by A19,XBOOLE_0:def
10
.= weight T by WAYBEL23:def 5;
A24: dom f = the carrier of T by FUNCT_2:def 1;
now let x1,x2 be set;
assume that
A25: x1 in dom f and
A26: x2 in dom f and
A27: f.x1 = f.x2;
reconsider x3 = x1, x4 = x2 as Point of T by A25,A26,FUNCT_2:def 1;
A28: f.x3 = meet { A where A is Element of the topology of T : x3 in A }
by A4;
A29: f.x4 = meet { A where A is Element of the topology of T : x4 in A }
by A4;
assume x1 <> x2;
then consider V be Subset of T such that
A30: V is open and
A31: (x3 in V & not x4 in V) or (x4 in V & not x3 in
V) by T_0TOPSP:def 7;
now per cases by A31;
suppose A32: x3 in V & not x4 in V;
V in the topology of T by A30,PRE_TOPC:def 5;
then A33: V in { A where A is Element of the topology of T : x3 in A }
by A32;
A34: meet { A where A is Element of the topology of T : x3 in A } c= V
proof
let z be set;
assume z in meet { A where A is Element of the topology of T :
x3 in A };
hence z in V by A33,SETFAM_1:def 1;
end;
the carrier of T in the topology of T by PRE_TOPC:def 1;
then A35: the carrier of T in { A where A is
Element of the topology of T : x4 in A };
now let Y be set;
assume Y in { A where A is Element of the topology of T : x4 in A };
then consider A be Element of the topology of T such that
A36: Y = A and
A37: x4 in A;
thus x4 in Y by A36,A37;
end;
then x4 in meet { A where A is Element of the topology of T : x3 in A }
by A27,A28,A29,A35,SETFAM_1:def
1;
hence contradiction by A32,A34;
suppose A38: x4 in V & not x3 in V;
V in the topology of T by A30,PRE_TOPC:def 5;
then A39: V in { A where A is Element of the topology of T : x4 in A }
by A38;
A40: meet { A where A is Element of the topology of T : x4 in A } c= V
proof
let z be set;
assume z in meet { A where A is Element of the topology of T :
x4 in A };
hence z in V by A39,SETFAM_1:def 1;
end;
the carrier of T in the topology of T by PRE_TOPC:def 1;
then A41: the carrier of T in { A where A is
Element of the topology of T : x3 in A };
now let Y be set;
assume Y in { A where A is Element of the topology of T : x3 in A };
then consider A be Element of the topology of T such that
A42: Y = A and
A43: x3 in A;
thus x3 in Y by A42,A43;
end;
then x3 in meet { A where A is Element of the topology of T : x4 in A }
by A27,A28,A29,A41,SETFAM_1:def
1;
hence contradiction by A38,A40;
end;
hence contradiction;
end;
then f is one-to-one by FUNCT_1:def 8;
then the carrier of T,rng f are_equipotent by A24,WELLORD2:def 4;
hence weight T = Card the carrier of T by A23,CARD_1:21;
end;
theorem Th11: :: PROPOSITION 4.6 (ii) (c)
for T be TopStruct
for L1 be continuous lower-bounded LATTICE st
InclPoset the topology of T = L1 & T is finite holds
CLweight L1 = Card the carrier of L1
proof
let T be TopStruct;
let L1 be continuous lower-bounded LATTICE;
assume A1: InclPoset the topology of T = L1;
assume A2: T is finite;
[#]L1 is with_bottom CLbasis of L1 by YELLOW15:26;
then the carrier of L1 is with_bottom CLbasis of L1 by PRE_TOPC:12;
then A3: Card the carrier of L1 in
{ Card B1 where B1 is with_bottom CLbasis of L1 : not contradiction };
A4: CLweight L1 c= Card the carrier of L1
proof
let z be set;
assume z in CLweight L1;
then z in meet { Card B1 where B1 is with_bottom CLbasis of L1 :
not contradiction } by Def1;
hence z in Card the carrier of L1 by A3,SETFAM_1:def 1;
end;
now let Z be set;
assume Z in { Card B1 where B1 is with_bottom CLbasis of L1 :
not contradiction };
then consider B1 be with_bottom CLbasis of L1 such that
A5: Z = Card B1;
the carrier of T is finite by A2,GROUP_1:def 13;
then the topology of T is finite by YELLOW15:3;
then the carrier of L1 is finite by A1,YELLOW_1:1;
then A6: L1 is finite by GROUP_1:def 13;
Bottom L1 in B1 by WAYBEL23:def 8;
then the carrier of CompactSublatt L1 c= B1 by WAYBEL23:48;
then Card the carrier of CompactSublatt L1 c= Card B1 by CARD_1:27;
hence Card the carrier of L1 c= Z by A5,A6,YELLOW15:27;
end;
then Card the carrier of L1 c= meet { Card B1 where B1 is
with_bottom CLbasis of L1 : not contradiction } by A3,SETFAM_1:6;
then Card the carrier of L1 c= CLweight L1 by Def1;
hence CLweight L1 = Card the carrier of L1 by A4,XBOOLE_0:def 10;
end;
theorem Th12:
for L1 be continuous lower-bounded sup-Semilattice
for T1 be Scott TopAugmentation of L1
for T2 be Lawson correct TopAugmentation of L1
for B2 be Basis of T2 holds
{ uparrow V where V is Subset of T2 : V in B2 } is Basis of T1
proof
let L1 be continuous lower-bounded sup-Semilattice;
let T1 be Scott TopAugmentation of L1;
let T2 be Lawson correct TopAugmentation of L1;
let B2 be Basis of T2;
A1: the RelStr of T1 = the RelStr of L1 &
the RelStr of T2 = the RelStr of L1 by YELLOW_9:def 4;
{ uparrow V where V is Subset of T2 : V in B2 } c= bool the carrier of T1
proof
let z be set;
assume z in { uparrow V where V is Subset of T2 : V in B2 };
then consider V be Subset of T2 such that
A2: z = uparrow V and
V in B2;
thus z in bool the carrier of T1 by A1,A2;
end;
then reconsider upV = { uparrow V where V is Subset of T2 : V in B2 } as
Subset-Family of T1 by SETFAM_1:def 7;
reconsider upV as Subset-Family of T1;
A3: upV c= the topology of T1
proof
let z be set;
assume z in upV;
then consider V be Subset of T2 such that
A4: z = uparrow V and
A5: V in B2;
A6: T1 is Scott TopAugmentation of T2 by A1,YELLOW_9:def 4;
B2 c= the topology of T2 by CANTOR_1:def 2;
then V in the topology of T2 by A5;
then V in lambda T2 by WAYBEL30:9;
then uparrow V in sigma T1 by A6,WAYBEL30:14;
hence z in the topology of T1 by A4,WAYBEL14:23;
end;
the topology of T1 c= UniCl upV
proof
let z be set;
assume A7: z in the topology of T1;
then reconsider z2 = z as Subset of T1;
A8: z in sigma T1 by A7,WAYBEL14:23;
A9: sigma T2 c= lambda T2 by WAYBEL30:10;
z in sigma T2 by A1,A8,YELLOW_9:52;
then z in lambda T2 by A9;
then A10: z in the topology of T2 by WAYBEL30:9;
reconsider z1 = z as Subset of T2 by A1,A7;
{ G where G is Subset of T2 : G in B2 & G c= z1 } c=
bool the carrier of T1
proof
let v be set;
assume v in { G where G is Subset of T2 : G in B2 & G c= z1 };
then consider G be Subset of T2 such that
A11: v = G and
G in B2 and
G c= z1;
thus v in bool the carrier of T1 by A1,A11;
end;
then reconsider Y1 = { G where G is Subset of T2 :
G in B2 & G c= z1 } as Subset-Family of T1
by SETFAM_1:def 7;
reconsider Y1 as Subset-Family of T1;
reconsider Y3 = Y1 as Subset-Family of T2 by A1;
{ uparrow G where G is Subset of T2 : G in B2 & G c= z1 } c=
bool the carrier of T1
proof
let v be set;
assume v in { uparrow G where G is Subset of T2 : G in B2 & G c= z1 };
then consider G be Subset of T2 such that
A12: v = uparrow G and
G in B2 and
G c= z1;
thus v in bool the carrier of T1 by A1,A12;
end;
then reconsider Y = { uparrow G where G is Subset of T2 :
G in B2 & G c= z1 } as Subset-Family of T1
by SETFAM_1:def 7;
reconsider Y as Subset-Family of T1;
A13: z1 is open by A10,PRE_TOPC:def 5;
z2 is open by A7,PRE_TOPC:def 5;
then z2 is upper by WAYBEL11:def 4;
then A14: uparrow z2 c= z2 by WAYBEL_0:24;
defpred P[set] means $1 in B2 & $1 c= z1;
A15: for S be Subset-Family of T2 st
S = { X where X is Subset of T2 : P[X]} holds
uparrow union S = union { uparrow X where X is Subset of T2: P[X]}
from UparrowUnion;
z2 c= uparrow z2 by WAYBEL_0:16;
then A16: z1 = uparrow z2 by A14,XBOOLE_0:def 10
.= uparrow union Y1 by A13,YELLOW_8:18
.= uparrow union Y3 by A1,WAYBEL_0:13
.= union Y by A15;
Y c= upV
proof
let v be set;
assume v in Y;
then consider G be Subset of T2 such that
A17: v = uparrow G and
A18: G in B2 and
G c= z1;
thus v in upV by A17,A18;
end;
hence z in UniCl upV by A16,CANTOR_1:def 1;
end;
hence { uparrow V where V is Subset of T2 : V in B2 } is Basis of T1
by A3,CANTOR_1:def 2;
end;
Lm1:
for L1 be continuous lower-bounded sup-Semilattice
for T1 be Scott TopAugmentation of L1
for T2 be Lawson correct TopAugmentation of L1 holds
weight T1 c= weight T2
proof
let L1 be continuous lower-bounded sup-Semilattice;
let T1 be Scott TopAugmentation of L1;
let T2 be Lawson correct TopAugmentation of L1;
consider B1 be Basis of T2 such that
A1: Card B1 = weight T2 by Th2;
{ uparrow V where V is Subset of T2 : V in B1 } is Basis of T1 by Th12;
then Card { uparrow V where V is Subset of T2 : V in B1 } in
{Card B2 where B2 is Basis of T1 : not contradiction};
then A2: meet {Card B2 where B2 is Basis of T1 : not contradiction} c=
Card { uparrow V where V is Subset of T2 : V in B1 } by SETFAM_1:4;
defpred P[set,set] means
ex y be Subset of T2 st y = $1 & $2 = uparrow y;
A3: for x be set st x in B1 ex z be set st P[x,z]
proof
let x be set;
assume x in B1;
then reconsider y = x as Subset of T2;
take uparrow y;
take y;
thus thesis;
end;
consider f be Function such that
A4: dom f = B1 and
A5: for x be set st x in B1 holds P[x,f.x] from NonUniqFuncEx(A3);
{ uparrow V where V is Subset of T2 : V in B1 } c= rng f
proof
let z be set;
assume z in { uparrow V where V is Subset of T2 : V in B1 };
then consider V be Subset of T2 such that
A6: z = uparrow V and
A7: V in B1;
consider V1 be Subset of T2 such that
A8: V1 = V and
A9: f.V = uparrow V1 by A5,A7;
thus z in rng f by A4,A6,A7,A8,A9,FUNCT_1:def 5;
end;
then Card { uparrow V where V is Subset of T2 : V in B1 } c= Card B1
by A4,CARD_1:28;
then meet {Card B2 where B2 is Basis of T1 : not contradiction} c=
Card B1 by A2,XBOOLE_1:1;
hence weight T1 c= weight T2 by A1,WAYBEL23:def 5;
end;
canceled;
theorem Th14:
for L1 be up-complete (non empty Poset) st L1 is finite
for x be Element of L1 holds
x in compactbelow x
proof
let L1 be up-complete (non empty Poset);
assume A1: L1 is finite;
let x be Element of L1;
x is compact & x <= x by A1,WAYBEL_3:17;
hence x in compactbelow x by WAYBEL_8:4;
end;
theorem Th15:
for L1 be finite LATTICE holds
L1 is arithmetic
proof
let L1 be finite LATTICE;
thus for x be Element of L1 holds compactbelow x is non empty directed;
thus L1 is up-complete;
thus L1 is satisfying_axiom_K
proof
let x be Element of L1;
for y be Element of L1 st y in compactbelow x holds y <= x by WAYBEL_8:4
;
then A1: x is_>=_than compactbelow x by LATTICE3:def 9;
now let y be Element of L1;
assume A2: y is_>=_than compactbelow x;
x in compactbelow x by Th14;
hence x <= y by A2,LATTICE3:def 9;
end;
hence x = sup compactbelow x by A1,YELLOW_0:30;
end;
thus CompactSublatt L1 is meet-inheriting
proof
let x,y be Element of L1;
assume that
x in the carrier of CompactSublatt L1 and
y in the carrier of CompactSublatt L1 and
ex_inf_of {x,y},L1;
x "/\" y is compact by WAYBEL_3:17;
then x "/\" y in the carrier of CompactSublatt L1 by WAYBEL_8:def 1;
hence inf {x,y} in the carrier of CompactSublatt L1 by YELLOW_0:40;
end;
end;
definition
cluster finite -> arithmetic LATTICE;
coherence by Th15;
end;
definition
cluster trivial reflexive transitive antisymmetric with_suprema with_infima
lower-bounded non empty finite strict RelStr;
existence
proof
0 in {0} by TARSKI:def 1;
then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:8;
reconsider T = RelStr(#{0},r#) as non empty RelStr;
take T;
thus T is trivial;
thus T is reflexive
proof
let x be Element of T;
x = 0 by TARSKI:def 1;
then [x,x] in {[0,0]} by TARSKI:def 1;
hence x <= x by ORDERS_1:def 9;
end;
then reconsider T' = T as trivial non empty reflexive RelStr;
T' is transitive;
hence T is transitive;
T' is antisymmetric;
hence T is antisymmetric;
T' is with_suprema;
hence T is with_suprema;
T' is with_infima;
hence T is with_infima;
reconsider T'' = T' as LATTICE;
T'' is lower-bounded;
hence T is lower-bounded;
thus T is non empty;
thus T is finite;
thus thesis;
end;
end;
theorem Th16:
for L1 be finite LATTICE
for B1 be with_bottom CLbasis of L1 holds
Card B1 = CLweight L1 iff B1 = the carrier of CompactSublatt L1
proof
let L1 be finite LATTICE;
let B1 be with_bottom CLbasis of L1;
thus Card B1 = CLweight L1 implies B1 = the carrier of CompactSublatt L1
proof
assume Card B1 = CLweight L1;
then A1: Card the carrier of CompactSublatt L1 = Card B1 by Th5;
A2: the carrier of CompactSublatt L1 c= B1 by WAYBEL23:72;
then the carrier of CompactSublatt L1 is finite by FINSET_1:13;
hence B1 = the carrier of CompactSublatt L1 by A1,A2,TRIANG_1:3;
end;
assume B1 = the carrier of CompactSublatt L1;
hence Card B1 = CLweight L1 by Th5;
end;
definition
let L1 be non empty reflexive RelStr;
let A be Subset of L1;
let a be Element of L1;
func Way_Up(a,A) -> Subset of L1 equals :Def2:
wayabove a \ uparrow A;
coherence;
end;
theorem
for L1 be non empty reflexive RelStr
for a be Element of L1 holds
Way_Up(a,{}(L1)) = wayabove a
proof
let L1 be non empty reflexive RelStr;
let a be Element of L1;
thus Way_Up(a,{}(L1)) = wayabove a \ uparrow {}(L1) by Def2
.= wayabove a;
end;
theorem
for L1 be non empty Poset
for A be Subset of L1
for a be Element of L1 st a in uparrow A holds
Way_Up(a,A) = {}
proof
let L1 be non empty Poset;
let A be Subset of L1;
let a be Element of L1;
assume A1: a in uparrow A;
A2: wayabove a c= uparrow A
proof
let z be set;
assume A3: z in wayabove a;
then reconsider z1 = z as Element of L1;
a << z1 by A3,WAYBEL_3:8;
then a <= z1 by WAYBEL_3:1;
hence z in uparrow A by A1,WAYBEL_0:def 20;
end;
thus Way_Up(a,A) = wayabove a \ uparrow A by Def2
.= {} by A2,XBOOLE_1:37;
end;
theorem Th19:
for L1 be non empty finite reflexive transitive RelStr holds
Ids L1 is finite
proof
let L1 be non empty finite reflexive transitive RelStr;
reconsider Y = bool the carrier of L1 as finite non empty set
by FINSET_1:24;
A1: { X where X is Ideal of L1 : not contradiction } c=
{ X where X is Element of Y : X is Ideal of L1 }
proof
let z be set;
assume z in { X where X is Ideal of L1 : not contradiction };
then consider X1 be Ideal of L1 such that
A2: z = X1;
thus z in { X where X is Element of Y : X is Ideal of L1 } by A2;
end;
A3: { X where X is Element of Y : X is Ideal of L1 } c=
{ X where X is Ideal of L1 : not contradiction }
proof
let z be set;
assume z in { X where X is Element of Y : X is Ideal of L1 };
then consider X1 be Element of Y such that
A4: z = X1 and
A5: X1 is Ideal of L1;
thus z in { X where X is Ideal of L1 : not contradiction } by A4,A5;
end;
A6: Ids L1 =
{ X where X is Ideal of L1 : not contradiction } by WAYBEL_0:def 23
.= { X where X is Element of Y : X is Ideal of L1 } by A1,A3,XBOOLE_0:def
10;
defpred P[set] means $1 is Ideal of L1;
deffunc F(set) = $1;
{F(X) where X is Element of Y : P[X]} is finite
from FraenkelFinIm;
hence Ids L1 is finite by A6;
end;
theorem Th20:
for L1 be continuous lower-bounded sup-Semilattice st L1 is infinite
for B1 be with_bottom CLbasis of L1 holds
B1 is infinite
proof
let L1 be continuous lower-bounded sup-Semilattice;
assume L1 is infinite;
then A1: the carrier of L1 is infinite by GROUP_1:def 13;
let B1 be with_bottom CLbasis of L1;
A2: dom supMap subrelstr B1 = Ids subrelstr B1 by WAYBEL23:51;
rng supMap subrelstr B1 = the carrier of L1 by WAYBEL23:65;
then Card the carrier of L1 c= Card Ids subrelstr B1 by A2,CARD_1:28;
then Ids subrelstr B1 is infinite by A1,CARD_2:68;
then subrelstr B1 is infinite by Th19;
then the carrier of subrelstr B1 is infinite by GROUP_1:def 13;
hence B1 is infinite by YELLOW_0:def 15;
end;
canceled 2;
theorem
for L1 be complete (non empty Poset)
for x be Element of L1 holds
x is compact implies x = inf wayabove x
proof
let L1 be complete (non empty Poset);
let x be Element of L1;
assume x is compact;
then x << x by WAYBEL_3:def 2;
then x in wayabove x by WAYBEL_3:8;
then A1: inf wayabove x <= x by YELLOW_2:24;
x <= inf wayabove x by WAYBEL14:9;
hence x = inf wayabove x by A1,YELLOW_0:def 3;
end;
theorem Th24:
for L1 be continuous lower-bounded sup-Semilattice st L1 is infinite
for B1 be with_bottom CLbasis of L1 holds
Card { Way_Up(a,A) where a is Element of L1, A is finite Subset of L1 :
a in B1 & A c= B1 } c= Card B1
proof
let L1 be continuous lower-bounded sup-Semilattice;
assume A1: L1 is infinite;
let B1 be with_bottom CLbasis of L1;
consider a1 be set such that
A2: a1 in B1 by XBOOLE_0:def 1;
reconsider a1 as Element of L1 by A2;
{}(L1) c= B1 by XBOOLE_1:2;
then Way_Up(a1,{}(L1)) in { Way_Up(a,A) where a is Element of L1,
A is finite Subset of L1 : a in B1 & A c= B1 } by A2;
then reconsider W_U = { Way_Up(a,A) where a is Element of L1,
A is finite Subset of L1 : a in B1 & A c= B1 } as non empty set;
B1 is infinite by A1,Th20;
then A3: Card B1 = Card (B1*) by CARD_4:87;
defpred P[Element of B1*,set] means
ex y be Element of L1, z be Subset of L1 st
y = $1/.1 & z = rng Del($1,1) & $2 = Way_Up(y,z);
A4: for x be Element of B1*
ex u be Element of W_U st P[x,u]
proof
let x be Element of B1*;
x/.1 in the carrier of L1 by TARSKI:def 3;
then reconsider y = x/.1 as Element of L1;
A5: rng Del(x,1) c= rng x by MATRLIN:2;
rng x c= B1 by FINSEQ_1:def 4;
then A6: rng Del(x,1) c= B1 by A5,XBOOLE_1:1;
then rng Del(x,1) c= the carrier of L1 by XBOOLE_1:1;
then reconsider z = rng Del(x,1) as Subset of L1;
Way_Up(y,z) in { Way_Up(a,A) where a is Element of L1,
A is finite Subset of L1 : a in B1 & A c= B1 } by A6;
then reconsider u = Way_Up(y,z) as Element of W_U;
take u,y,z;
thus thesis;
end;
consider f be Function of B1*,W_U such that
A7: for x be Element of B1* holds P[x,f.x] from FuncExD(A4);
A8: dom f = B1* by FUNCT_2:def 1;
W_U c= rng f
proof
let z be set;
assume z in W_U;
then consider a be Element of L1, A be finite Subset of L1 such that
A9: z = Way_Up(a,A) and
A10: a in B1 and
A11: A c= B1;
consider p be FinSequence such that
A12: A = rng p by FINSEQ_1:73;
reconsider p as FinSequence of B1 by A11,A12,FINSEQ_1:def 4;
reconsider a1 = a as Element of B1 by A10;
set q = <*a1*>^p;
A13: q in B1* by FINSEQ_1:def 11;
then consider y be Element of L1,
v be Subset of L1 such that
A14: y = q/.1 and
A15: v = rng Del(q,1) and
A16: f.q = Way_Up(y,v) by A7;
A17: a = y by A14,FINSEQ_5:16;
A = v by A12,A15,WSIERP_1:48;
hence z in rng f by A8,A9,A13,A16,A17,FUNCT_1:def 5;
end;
hence thesis by A3,A8,CARD_1:28;
end;
theorem Th25:
for T be Lawson (complete TopLattice)
for X be finite Subset of T holds
(uparrow X)` is open & (downarrow X)` is open
proof
let T be Lawson (complete TopLattice);
let X be finite Subset of T;
{ uparrow x where x is Element of T : x in X } c= bool the carrier of T
proof
let z be set;
assume z in { uparrow x where x is Element of T : x in X };
then consider x be Element of T such that
A1: z = uparrow x and
x in X;
thus z in bool the carrier of T by A1;
end;
then reconsider upx = { uparrow x where x is Element of T : x in X }
as Subset-Family of T by SETFAM_1:def 7;
reconsider upx as Subset-Family of T;
{ downarrow x where x is Element of T : x in X } c= bool the carrier of T
proof
let z be set;
assume z in { downarrow x where x is Element of T : x in X };
then consider x be Element of T such that
A2: z = downarrow x and
x in X;
thus z in bool the carrier of T by A2;
end;
then reconsider dox = { downarrow x where x is Element of T : x in X }
as Subset-Family of T by SETFAM_1:def 7;
reconsider dox as Subset-Family of T;
now let P be Subset of T;
assume P in upx;
then consider x be Element of T such that
A3: P = uparrow x and
x in X;
thus P is closed by A3,WAYBEL19:38;
end;
then A4: upx is closed by TOPS_2:def 2;
A5: X is finite;
deffunc F(Element of T) = uparrow $1;
A6: {F(x) where x is Element of T : x in X }
is finite from FraenkelFin(A5);
uparrow X = union upx by YELLOW_9:4;
then uparrow X is closed by A4,A6,TOPS_2:28;
hence (uparrow X)` is open by TOPS_1:29;
now let P be Subset of T;
assume P in dox;
then consider x be Element of T such that
A7: P = downarrow x and
x in X;
thus P is closed by A7,WAYBEL19:38;
end;
then A8: dox is closed by TOPS_2:def 2;
deffunc F(Element of T) = downarrow $1;
A9: {F(x) where x is Element of T : x in X }
is finite from FraenkelFin(A5);
downarrow X = union dox by YELLOW_9:4;
then downarrow X is closed by A8,A9,TOPS_2:28;
hence (downarrow X)` is open by TOPS_1:29;
end;
theorem Th26:
for L1 be continuous lower-bounded sup-Semilattice
for T be Lawson correct TopAugmentation of L1 holds
for B1 be with_bottom CLbasis of L1 holds
{ Way_Up(a,A) where a is Element of L1, A is finite Subset of L1 :
a in B1 & A c= B1 } is Basis of T
proof
let L1 be continuous lower-bounded sup-Semilattice;
let T be Lawson correct TopAugmentation of L1;
let B1 be with_bottom CLbasis of L1;
A1: the RelStr of L1 = the RelStr of T by YELLOW_9:def 4;
{ Way_Up(a,A) where a is Element of L1,
A is finite Subset of L1 : a in B1 & A c= B1 } c= bool the carrier of T
proof
let z be set;
assume z in { Way_Up(a,A) where a is Element of L1,
A is finite Subset of L1 : a in B1 & A c= B1 };
then consider a be Element of L1, A be finite Subset of L1 such that
A2: z = Way_Up(a,A) and
a in B1 and
A c= B1;
thus z in bool the carrier of T by A1,A2;
end;
then reconsider W_U = { Way_Up(a,A) where a is Element of L1,
A is finite Subset of L1 : a in B1 & A c= B1 }
as Subset-Family of T by SETFAM_1:def 7;
reconsider W_U as Subset-Family of T;
A3: W_U c= the topology of T
proof
let z be set;
assume z in W_U;
then consider a be Element of L1, A be finite Subset of L1 such that
A4: z = Way_Up(a,A) and
a in B1 and
A c= B1;
reconsider a1 = a as Element of T by A1;
reconsider A1 = A as finite Subset of T by A1;
A5: wayabove a1 is open by WAYBEL19:40;
(uparrow A1)` is open by Th25;
then A6: wayabove a1 /\ (uparrow A1)` is open by A5,TOPS_1:38;
z = wayabove a \ uparrow A by A4,Def2
.= wayabove a1 \ uparrow A by A1,YELLOW12:13
.= wayabove a1 \ uparrow A1 by A1,WAYBEL_0:13
.= wayabove a1 /\ (uparrow A1)` by SUBSET_1:32;
hence z in the topology of T by A6,PRE_TOPC:def 5;
end;
now let A be Subset of T;
assume A7: A is open;
let pT be Point of T;
assume A8: pT in A;
consider S be Scott TopAugmentation of T;
A9: the RelStr of S = the RelStr of T by YELLOW_9:def 4;
reconsider BL = { W \ uparrow F where W,F is Subset of T : W in sigma T &
F is finite} as Basis of T by WAYBEL19:32;
consider a be Subset of T such that
A10: a in BL and
A11: pT in a and
A12: a c= A by A7,A8,YELLOW_9:31;
consider W,FT be Subset of T such that
A13: a = W \ uparrow FT and
A14: W in sigma T and
A15: FT is finite by A10;
reconsider W1 = W as Subset of S by A9;
sigma S = sigma T by A9,YELLOW_9:52;
then A16: W = union { wayabove x where x is Element of S : x in W1 }
by A14,WAYBEL14:33;
A17: pT in W & not pT in uparrow FT by A11,A13,XBOOLE_0:def 4;
then consider k be set such that
A18: pT in k and
A19: k in { wayabove x where x is Element of S : x in W1 }
by A16,TARSKI:def 4;
consider xS be Element of S such that
A20: k = wayabove xS and
A21: xS in W1 by A19;
reconsider pS = pT as Element of S by A9;
reconsider pL = pS as Element of L1 by A1;
reconsider xL = xS as Element of L1 by A1,A9;
reconsider FL = FT as Subset of L1 by A1;
xS << pS by A18,A20,WAYBEL_3:8;
then A22: xL << pL by A1,A9,WAYBEL_8:8;
Bottom L1 in B1 by WAYBEL23:def 8;
then consider bL be Element of L1 such that
A23: bL in B1 and
A24: xL <= bL and
A25: bL << pL by A22,WAYBEL23:47;
A26: pL in wayabove bL by A25,WAYBEL_3:8;
A27: uparrow FT = uparrow FL by A1,WAYBEL_0:13;
defpred P[set,set] means ex b1,y1 be Element of L1 st
y1 = $1 & b1 = $2 & b1 in B1 & not b1 <= pL & b1 << y1;
A28: for y be set st y in FL ex b be set st P[y,b]
proof
let y be set;
assume A29: y in FL;
then reconsider y1 = y as Element of L1;
not y1 <= pL by A17,A27,A29,WAYBEL_0:def 16;
then consider b1 be Element of L1 such that
A30: b1 in B1 and
A31: not b1 <= pL and
A32: b1 << y1 by WAYBEL23:46;
reconsider b = b1 as set;
take b,b1,y1;
thus thesis by A30,A31,A32;
end;
consider f be Function such that
A33: dom f = FL and
A34: for y be set st y in FL holds P[y,f.y] from NonUniqFuncEx(A28);
rng f c= the carrier of L1
proof
let z be set;
assume z in rng f;
then consider v be set such that
A35: v in dom f and
A36: z = f.v by FUNCT_1:def 5;
consider b1,y1 be Element of L1 such that
y1 = v and
A37: b1 = f.v and
b1 in B1 and
not b1 <= pL and
b1 << y1 by A33,A34,A35;
thus z in the carrier of L1 by A36,A37;
end;
then reconsider FFL = rng f as Subset of L1;
reconsider cT = wayabove bL \ uparrow FFL as Subset of T
by A1;
take cT;
A38: cT = Way_Up(bL,FFL) by Def2;
A39: FFL is finite by A15,A33,FINSET_1:26;
FFL c= B1
proof
let z be set;
assume z in FFL;
then consider v be set such that
A40: v in dom f and
A41: z = f.v by FUNCT_1:def 5;
consider b1,y1 be Element of L1 such that
y1 = v and
A42: b1 = f.v and
A43: b1 in B1 and
not b1 <= pL and
b1 << y1 by A33,A34,A40;
thus z in B1 by A41,A42,A43;
end;
hence cT in W_U by A23,A38,A39;
for z be Element of L1 holds not z in FFL or not z <= pL
proof
let z be Element of L1;
assume z in FFL;
then consider v be set such that
A44: v in dom f and
A45: z = f.v by FUNCT_1:def 5;
consider b1,y1 be Element of L1 such that
y1 = v and
A46: b1 = f.v and
b1 in B1 and
A47: not b1 <= pL and
b1 << y1 by A33,A34,A44;
thus not z <= pL by A45,A46,A47;
end;
then for z be Element of L1 holds not z <= pL or not z in FFL;
then not pL in uparrow FFL by WAYBEL_0:def 16;
hence pT in cT by A26,XBOOLE_0:def 4;
A48: wayabove bL c= wayabove xL by A24,WAYBEL_3:12;
uparrow FL c= uparrow FFL
proof
let z be set;
assume A49: z in uparrow FL;
then reconsider z1 = z as Element of L1;
consider v1 be Element of L1 such that
A50: v1 <= z1 and
A51: v1 in FL by A49,WAYBEL_0:def 16;
consider b1,y1 be Element of L1 such that
A52: y1 = v1 and
A53: b1 = f.v1 and
b1 in B1 and
not b1 <= pL and
A54: b1 << y1 by A34,A51;
A55: b1 in FFL by A33,A51,A53,FUNCT_1:def 5;
b1 << z1 by A50,A52,A54,WAYBEL_3:2;
then b1 <= z1 by WAYBEL_3:1;
hence z in uparrow FFL by A55,WAYBEL_0:def 16;
end;
then A56: wayabove bL \ uparrow FFL c= wayabove xL \ uparrow FL
by A48,XBOOLE_1:35
;
wayabove xL c= W
proof
let z be set;
assume A57: z in wayabove xL;
wayabove xL = wayabove xS by A1,A9,YELLOW12:13;
then wayabove xL in { wayabove x where x is Element of S : x in W1 }
by A21;
hence z in W by A16,A57,TARSKI:def 4;
end;
then wayabove xL \ uparrow FL c= a by A13,A27,XBOOLE_1:33;
then wayabove bL \ uparrow FFL c= a by A56,XBOOLE_1:1;
hence cT c= A by A12,XBOOLE_1:1;
end;
hence thesis by A3,YELLOW_9:32;
end;
Lm2:
for L1 be continuous lower-bounded sup-Semilattice
for T be Lawson correct TopAugmentation of L1 holds
weight T c= CLweight L1
proof
let L1 be continuous lower-bounded sup-Semilattice;
let T be Lawson correct TopAugmentation of L1;
A1: the RelStr of T = the RelStr of L1 by YELLOW_9:def 4;
consider B1 be with_bottom CLbasis of L1 such that
A2: Card B1 = CLweight L1 by Th4;
now per cases;
suppose A3: L1 is finite;
then the carrier of L1 is finite by GROUP_1:def 13;
then A4: T is finite by A1,GROUP_1:def 13;
B1 = the carrier of CompactSublatt L1 by A2,A3,Th16
.= the carrier of L1 by A3,YELLOW15:27;
hence weight T c= CLweight L1 by A1,A2,A4,Th10;
suppose A5: L1 is infinite;
set W_U = { Way_Up(a,A) where a is Element of L1,
A is finite Subset of L1 : a in B1 & A c= B1 };
A6: Card W_U c= CLweight L1 by A2,A5,Th24;
W_U is Basis of T by Th26;
then weight T c= Card W_U by Th1;
hence weight T c= CLweight L1 by A6,XBOOLE_1:1;
end;
hence weight T c= CLweight L1;
end;
theorem Th27:
for L1 be continuous lower-bounded sup-Semilattice
for T be Scott TopAugmentation of L1
for b be Basis of T holds
{ wayabove inf u where u is Subset of T : u in b } is Basis of T
proof
let L1 be continuous lower-bounded sup-Semilattice;
let T be Scott TopAugmentation of L1;
let b be Basis of T;
reconsider b1 = { wayabove x where x is Element of T: not contradiction }
as Basis of T by WAYBEL11:45;
set b2 = { wayabove inf u where u is Subset of T : u in b };
b2 c= bool the carrier of T
proof
let z be set;
assume z in b2;
then consider u be Subset of T such that
A1: z = wayabove inf u and
u in b;
thus z in bool the carrier of T by A1;
end;
then b2 is Subset-Family of T by SETFAM_1:def 7;
then reconsider b2 as Subset-Family of T;
A2: b2 c= the topology of T
proof
let z be set;
assume z in b2;
then consider u be Subset of T such that
A3: z = wayabove inf u and
u in b;
wayabove inf u is open by WAYBEL11:36;
hence z in the topology of T by A3,PRE_TOPC:def 5;
end;
now let A be Subset of T;
assume A4: A is open;
let a be Point of T;
assume a in A;
then consider C be Subset of T such that
A5: C in b1 and
A6: a in C and
A7: C c= A by A4,YELLOW_9:31;
consider x be Element of T such that
A8: C = wayabove x by A5;
C is open by A5,YELLOW_8:19;
then consider D be Subset of T such that
A9: D in b and
A10: a in D and
A11: D c= C by A6,YELLOW_9:31;
reconsider a1 = a as Element of T;
D is open by A9,YELLOW_8:19;
then consider E be Subset of T such that
A12: E in b1 and
A13: a in E and
A14: E c= D by A10,YELLOW_9:31;
consider z be Element of T such that
A15: E = wayabove z by A12;
take u = wayabove inf D;
thus u in b2 by A9;
z << a1 by A13,A15,WAYBEL_3:8;
then consider y be Element of T such that
A16: z << y and
A17: y << a1 by WAYBEL_4:53;
A18: inf D is_<=_than D by YELLOW_0:33;
y in wayabove z by A16,WAYBEL_3:8;
then inf D <= y by A14,A15,A18,LATTICE3:def 8;
then inf D << a1 by A17,WAYBEL_3:2;
hence a in u by WAYBEL_3:8;
A19: ex_inf_of uparrow x,T & ex_inf_of D,T by YELLOW_0:17;
wayabove x c= uparrow x by WAYBEL_3:11;
then D c= uparrow x by A8,A11,XBOOLE_1:1;
then inf uparrow x <= inf D by A19,YELLOW_0:35;
then x <= inf D by WAYBEL_0:39;
then wayabove inf D c= C by A8,WAYBEL_3:12;
hence u c= A by A7,XBOOLE_1:1;
end;
hence thesis by A2,YELLOW_9:32;
end;
theorem Th28:
for L1 be continuous lower-bounded sup-Semilattice
for T be Scott TopAugmentation of L1
for B1 be Basis of T st B1 is infinite holds
{ inf u where u is Subset of T : u in B1 } is infinite
proof
let L1 be continuous lower-bounded sup-Semilattice;
let T be Scott TopAugmentation of L1;
let B1 be Basis of T;
assume that
A1: B1 is infinite and
A2: { inf u where u is Subset of T : u in B1 } is finite;
reconsider B2 = { inf u where u is Subset of T : u in B1 } as set;
reconsider B3 = { wayabove inf u where u is Subset of T : u in B1 }
as Basis of T by Th27;
defpred P[set,set] means
ex y be Element of T st $1 = y & $2 = wayabove y;
A3: for x be set st x in B2 ex y be set st y in B3 & P[x,y]
proof
let x be set;
assume x in B2;
then consider u1 be Subset of T such that
A4: x = inf u1 and
A5: u1 in B1;
reconsider z = x as Element of T by A4;
take y = wayabove z;
thus y in B3 by A4,A5;
take z;
thus thesis;
end;
consider f be Function such that
A6: dom f = B2 and
A7: rng f c= B3 and
A8: for x be set st x in B2 holds P[x,f.x]
from NonUniqBoundFuncEx(A3);
B3 c= rng f
proof
let z be set;
assume z in B3;
then consider u1 be Subset of T such that
A9: z = wayabove inf u1 and
A10: u1 in B1;
inf u1 in B2 by A10;
then consider y be Element of T such that
A11: inf u1 = y and
A12: f.(inf u1) = wayabove y by A8;
z = f.(inf u1) & inf u1 in B2 by A9,A10,A11,A12;
hence z in rng f by A6,FUNCT_1:def 5;
end;
then rng f = B3 by A7,XBOOLE_0:def 10;
then B3 is finite by A2,A6,FINSET_1:26;
then T is finite by YELLOW15:31;
then the carrier of T is finite by GROUP_1:def 13;
hence contradiction by A1,YELLOW15:3;
end;
Lm3:
for L1 be continuous lower-bounded sup-Semilattice
for T be Scott TopAugmentation of L1 holds
CLweight L1 c= weight T
proof
let L1 be continuous lower-bounded sup-Semilattice;
let T be Scott TopAugmentation of L1;
consider B1 be Basis of T such that
A1: Card B1 = weight T by Th2;
{ inf u where u is Subset of T : u in B1 } c= the carrier of T
proof
let z be set;
assume z in { inf u where u is Subset of T : u in B1 };
then consider u be Subset of T such that
A2: z = inf u and
u in B1;
thus z in the carrier of T by A2;
end;
then reconsider B0 = { inf u where u is Subset of T : u in B1 }
as Subset of T;
defpred P[set,set] means ex y be Subset of T st $1 = y & $2 = inf y;
A3: for x be set st x in B1 ex y be set st y in B0 & P[x,y]
proof
let x be set;
assume A4: x in B1;
then reconsider z = x as Subset of T;
take y = inf z;
thus y in B0 by A4;
take z;
thus thesis;
end;
consider f be Function such that
A5: dom f = B1 and
rng f c= B0 and
A6: for x be set st x in B1 holds P[x,f.x] from NonUniqBoundFuncEx(A3);
B0 c= rng f
proof
let z be set;
assume z in B0;
then consider u be Subset of T such that
A7: z = inf u and
A8: u in B1;
consider y be Subset of T such that
A9: u = y and
A10: f.u = inf y by A6,A8;
thus z in rng f by A5,A7,A8,A9,A10,FUNCT_1:def 5;
end;
then A11: Card B0 c= Card B1 by A5,CARD_1:28;
set B2 = finsups B0;
A12: the RelStr of L1 = the RelStr of T by YELLOW_9:def 4;
A13: now per cases;
suppose A14: L1 is finite;
A15: B0 c= B2 by WAYBEL_0:50;
the carrier of L1 c= B0
proof
let z be set;
assume z in the carrier of L1;
then reconsider z1 = z as Element of T by A12;
the carrier of T is finite by A12,A14,GROUP_1:def 13;
then T is finite by GROUP_1:def 13;
then A16: uparrow z1 is open by WAYBEL11:def 5;
z1 <= z1;
then z1 in uparrow z1 by WAYBEL_0:18;
then consider A be Subset of T such that
A17: A in B1 and
A18: z1 in A and
A19: A c= uparrow z1 by A16,YELLOW_9:31;
ex_inf_of uparrow z1,T & ex_inf_of A,T by YELLOW_0:17;
then inf uparrow z1 <= inf A by A19,YELLOW_0:35;
then A20: z1 <= inf A by WAYBEL_0:39;
inf A <= z1 by A18,YELLOW_2:24;
then z = inf A by A20,YELLOW_0:def 3;
hence z in B0 by A17;
end;
then B2 c= B0 by A12,XBOOLE_1:1;
hence Card B2 = Card B0 by A15,XBOOLE_0:def 10;
suppose L1 is infinite;
then the carrier of L1 is infinite by GROUP_1:def 13;
then T is infinite by A12,GROUP_1:def 13;
then B1 is infinite by YELLOW15:31;
then B0 is infinite by Th28;
hence Card B2 = Card B0 by YELLOW15:28;
end;
A21: ex_sup_of {},T by YELLOW_0:42;
{} is finite Subset of B0 by XBOOLE_1:2;
then "\/"({},T) in {"\/"
(Y,T) where Y is finite Subset of B0: ex_sup_of Y,T}
by A21;
then "\/"({},T) in finsups B0 by WAYBEL_0:def 27;
then "\/"({},L1) in finsups B0 by A12,A21,YELLOW_0:26;
then A22: Bottom L1 in B2 by YELLOW_0:def 11;
reconsider B2 as Subset of L1 by A12;
now let x,y be Element of L1;
assume that
A23: x in B2 and
A24: y in B2;
A25: x in { "\/"(Y,T) where Y is finite Subset of B0 : ex_sup_of Y,T } &
y in { "\/"(Y,T) where Y is finite Subset of B0 : ex_sup_of Y,T }
by A23,A24,WAYBEL_0:def 27;
then consider Y1 be finite Subset of B0 such that
A26: x = "\/"(Y1,T) and
A27: ex_sup_of Y1,T;
consider Y2 be finite Subset of B0 such that
A28: y = "\/"(Y2,T) and
A29: ex_sup_of Y2,T by A25;
A30: ex_sup_of Y1 \/ Y2,T by YELLOW_0:17;
sup {x,y} = x "\/" y by YELLOW_0:41
.= "\/"(Y1,T) "\/" "\/"(Y2,T) by A12,A26,A28,YELLOW12:10
.= "\/"(Y1 \/ Y2,T) by A27,A29,YELLOW_2:3;
then sup {x,y} in
{ "\/"(Y,T) where Y is finite Subset of B0 : ex_sup_of Y,T } by A30;
hence sup {x,y} in B2 by WAYBEL_0:def 27;
end;
then reconsider B2 as join-closed Subset of L1 by WAYBEL23:18;
for x,y be Element of L1 st x << y
ex b be Element of L1 st b in B2 & x <= b & b << y
proof
let x,y be Element of L1;
reconsider x1 = x, y1 = y as Element of T by A12;
assume x << y;
then y in wayabove x by WAYBEL_3:8;
then A31: y1 in wayabove x1 by A12,YELLOW12:13;
wayabove x1 is open by WAYBEL11:36;
then consider u be Subset of T such that
A32: u in B1 and
A33: y1 in u and
A34: u c= wayabove x1 by A31,YELLOW_9:31;
reconsider b = inf u as Element of L1 by A12;
take b;
A35: b in B0 by A32;
B0 c= B2 by WAYBEL_0:50;
hence b in B2 by A35;
A36: ex_inf_of uparrow x1,T & ex_inf_of u,T by YELLOW_0:17;
wayabove x1 c= uparrow x1 by WAYBEL_3:11;
then u c= uparrow x1 by A34,XBOOLE_1:1;
then inf uparrow x1 <= inf u by A36,YELLOW_0:35;
then x1 <= inf u by WAYBEL_0:39;
hence x <= b by A12,YELLOW_0:1;
u is open by A32,YELLOW_8:19;
then inf u << y1 by A33,WAYBEL14:26;
hence b << y by A12,WAYBEL_8:8;
end;
then A37: B2 is CLbasis of L1 by A22,WAYBEL23:47;
B2 is with_bottom by A22,WAYBEL23:def 8;
then CLweight L1 c= Card B0 by A13,A37,Th3;
hence CLweight L1 c= weight T by A1,A11,XBOOLE_1:1;
end;
theorem Th29: :: THEOREM 4.7 (1)=(2)
for L1 be continuous lower-bounded sup-Semilattice
for T be Scott TopAugmentation of L1 holds
CLweight L1 = weight T
proof
let L1 be continuous lower-bounded sup-Semilattice;
let T be Scott TopAugmentation of L1;
consider T1 be Lawson correct TopAugmentation of L1;
A1: CLweight L1 c= weight T by Lm3;
A2: weight T c= weight T1 by Lm1;
weight T1 c= CLweight L1 by Lm2;
then weight T c= CLweight L1 by A2,XBOOLE_1:1;
hence CLweight L1 = weight T by A1,XBOOLE_0:def 10;
end;
theorem :: THEOREM 4.7 (1)=(3)
for L1 be continuous lower-bounded sup-Semilattice
for T be Lawson correct TopAugmentation of L1 holds
CLweight L1 = weight T
proof
let L1 be continuous lower-bounded sup-Semilattice;
let T be Lawson correct TopAugmentation of L1;
consider T1 be Scott TopAugmentation of L1;
A1: weight T c= CLweight L1 by Lm2;
A2: CLweight L1 c= weight T1 by Lm3;
weight T1 c= weight T by Lm1;
then CLweight L1 c= weight T by A2,XBOOLE_1:1;
hence CLweight L1 = weight T by A1,XBOOLE_0:def 10;
end;
theorem Th31:
for L1,L2 be non empty RelStr st L1,L2 are_isomorphic holds
Card the carrier of L1 = Card the carrier of L2
proof
let L1,L2 be non empty RelStr;
assume L1,L2 are_isomorphic;
then consider f be map of L1,L2 such that
A1: f is isomorphic by WAYBEL_1:def 8;
A2: dom f = the carrier of L1 by FUNCT_2:def 1;
f is one-to-one & rng f = the carrier of L2 by A1,WAYBEL_0:66;
then the carrier of L1,the carrier of L2 are_equipotent
by A2,WELLORD2:def 4;
hence thesis by CARD_1:21;
end;
theorem :: THEOREM 4.7 (1)=(4)
for L1 be continuous lower-bounded sup-Semilattice
for B1 be with_bottom CLbasis of L1 st Card B1 = CLweight L1 holds
CLweight L1 = CLweight InclPoset Ids subrelstr B1
proof
let L1 be continuous lower-bounded sup-Semilattice;
let B1 be with_bottom CLbasis of L1;
assume A1: Card B1 = CLweight L1;
CompactSublatt InclPoset Ids subrelstr B1,subrelstr B1 are_isomorphic
by WAYBEL23:70;
then A2: Card the carrier of CompactSublatt InclPoset Ids subrelstr B1 =
Card the carrier of subrelstr B1 by Th31;
thus CLweight InclPoset Ids subrelstr B1 =
Card the carrier of CompactSublatt InclPoset Ids subrelstr B1 by Th5
.= CLweight L1 by A1,A2,YELLOW_0:def 15;
end;
definition
let L1 be continuous lower-bounded sup-Semilattice;
cluster InclPoset sigma L1 -> with_suprema continuous;
coherence
proof
consider S be Scott TopAugmentation of L1;
A1: the RelStr of S = the RelStr of L1 by YELLOW_9:def 4;
InclPoset sigma S is complete;
hence InclPoset sigma L1 is with_suprema by A1,YELLOW_9:52;
InclPoset sigma S is continuous by WAYBEL14:36;
hence thesis by A1,YELLOW_9:52;
end;
end;
theorem :: THEOREM 4.7 (5)
for L1 be continuous lower-bounded sup-Semilattice holds
CLweight L1 c= CLweight InclPoset sigma L1
proof
let L1 be continuous lower-bounded sup-Semilattice;
consider S be Scott TopAugmentation of L1;
A1: the RelStr of S = the RelStr of L1 by YELLOW_9:def 4;
A2: CLweight L1 = weight S by Th29;
A3: InclPoset the topology of S = InclPoset sigma L1 by YELLOW_9:51;
now per cases;
suppose L1 is infinite;
then the carrier of S is infinite by A1,GROUP_1:def 13;
then S is infinite by GROUP_1:def 13;
hence CLweight L1 c= CLweight InclPoset sigma L1 by A2,A3,Th8;
suppose L1 is finite;
then the carrier of S is finite by A1,GROUP_1:def 13;
then A4: S is finite by GROUP_1:def 13;
A5: Card the carrier of S c= Card the carrier of InclPoset sigma L1
by A3,Th9;
weight S = Card the carrier of S by A4,Th10;
hence CLweight L1 c= CLweight InclPoset sigma L1 by A2,A3,A4,A5,Th11;
end;
hence thesis;
end;
theorem :: THEOREM 4.7 (6)
for L1 be continuous lower-bounded sup-Semilattice st L1 is infinite holds
CLweight L1 = CLweight InclPoset sigma L1
proof
let L1 be continuous lower-bounded sup-Semilattice;
consider S be Scott TopAugmentation of L1;
A1: the RelStr of S = the RelStr of L1 by YELLOW_9:def 4;
assume A2: L1 is infinite;
A3: CLweight L1 = weight S by Th29;
A4: InclPoset the topology of S = InclPoset sigma L1 by YELLOW_9:51;
the carrier of S is infinite by A1,A2,GROUP_1:def 13;
then S is infinite by GROUP_1:def 13;
hence thesis by A3,A4,Th8;
end;