:: Weights of Continuous Lattices
:: by Robert Milewski
::
:: Received January 6, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ORDERS_2, SETFAM_1, SUBSET_1, WAYBEL_0, TARSKI, XXREAL_0,
LATTICES, ORDINAL2, WAYBEL23, YELLOW_1, YELLOW_0, WAYBEL_8, CARD_1,
ORDINAL1, STRUCT_0, XBOOLE_0, PRE_TOPC, RLVECT_3, RCOMP_1, WAYBEL_3,
FINSET_1, EQREL_1, ZFMISC_1, FUNCT_1, RELAT_1, WAYBEL11, YELLOW_9,
WAYBEL19, PRELAMB, CANTOR_1, PROB_1, DIRAF, LATTICE3, RELAT_2, CARD_FIL,
REWRITE1, PARTFUN1, FINSEQ_3, FINSEQ_1, ORDINAL4, WAYBEL_9, WELLORD1,
CAT_1, WAYBEL31;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FINSET_1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, DOMAIN_1, FINSEQ_2, FINSEQ_3,
ORDINAL1, CARD_1, STRUCT_0, PRE_TOPC, TOPS_2, CANTOR_1, ORDERS_2,
LATTICE3, YELLOW_0, YELLOW_1, YELLOW_9, WAYBEL_0, WAYBEL_1, WAYBEL_3,
WAYBEL_8, WAYBEL_9, WAYBEL11, WAYBEL19, WAYBEL23;
constructors DOMAIN_1, NAT_1, FINSEQ_3, TOPS_2, CANTOR_1, WAYBEL_1, WAYBEL_8,
WAYBEL11, YELLOW_9, WAYBEL19, WAYBEL23, RELSET_1, WAYBEL_2;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, CARD_1, FINSEQ_1,
STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, YELLOW_3,
WAYBEL_3, WAYBEL_4, WAYBEL_8, WAYBEL14, YELLOW_9, YELLOW11, WAYBEL19,
WAYBEL23, YELLOW15, WAYBEL25, WAYBEL30, ORDINAL1, PRE_TOPC;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, YELLOW_0, WAYBEL_8;
equalities YELLOW_0, WAYBEL_8, STRUCT_0;
expansions TARSKI;
theorems TARSKI, SETFAM_1, SUBSET_1, FINSET_1, RELSET_1, FUNCT_1, FUNCT_2,
FINSEQ_1, FINSEQ_5, CARD_1, CARD_4, WELLORD2, T_0TOPSP, ORDERS_2,
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, FINSEQ_3,
CARD_2;
schemes ORDINAL1, FUNCT_2, PRE_CIRC, CLASSES1, FRAENKEL, FUNCT_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: union { uparrow X where X is Subset of L1() : P[X] } c= uparrow union S
proof
let z be object;
assume z in union { uparrow X where X is Subset of L1() : P[X] };
then consider Z be set such that
A3: z in Z and
A4: Z in { uparrow X where X is Subset of L1() : P[X] } by TARSKI:def 4;
consider X1 be Subset of L1() such that
A5: Z = uparrow X1 and
A6: P[X1] by A4;
reconsider z1 = z as Element of L1() by A3,A5;
consider y1 be Element of L1() such that
A7: y1 <= z1 and
A8: y1 in X1 by A3,A5,WAYBEL_0:def 16;
X1 in S by A1,A6;
then y1 in union S by A8,TARSKI:def 4;
hence thesis by A7,WAYBEL_0:def 16;
end;
uparrow union S c= union { uparrow X where X is Subset of L1() : P[X]}
proof
let z be object;
assume
A9: z in uparrow union S;
then reconsider z1 = z as Element of L1();
consider y1 be Element of L1() such that
A10: y1 <= z1 and
A11: y1 in union S by A9,WAYBEL_0:def 16;
consider Z be set such that
A12: y1 in Z and
A13: Z in S by A11,TARSKI:def 4;
consider X1 be Subset of L1() such that
A14: Z = X1 and
A15: P[X1] by A1,A13;
A16: uparrow X1 in { uparrow X where X is Subset of L1() : P[X] } by A15;
z in uparrow X1 by A10,A12,A14,WAYBEL_0:def 16;
hence thesis by A16,TARSKI:def 4;
end;
hence thesis 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: union { downarrow X where X is Subset of L1(): P[X] } c= downarrow union S
proof
let z be object;
assume z in union { downarrow X where X is Subset of L1() : P[X] };
then consider Z be set such that
A3: z in Z and
A4: Z in { downarrow X where X is Subset of L1(): P[X]} by TARSKI:def 4;
consider X1 be Subset of L1() such that
A5: Z = downarrow X1 and
A6: P[X1] by A4;
reconsider z1 = z as Element of L1() by A3,A5;
consider y1 be Element of L1() such that
A7: y1 >= z1 and
A8: y1 in X1 by A3,A5,WAYBEL_0:def 15;
X1 in S by A1,A6;
then y1 in union S by A8,TARSKI:def 4;
hence thesis by A7,WAYBEL_0:def 15;
end;
downarrow union S c= union { downarrow X where X is Subset of L1() : P[X ] }
proof
let z be object;
assume
A9: z in downarrow union S;
then reconsider z1 = z as Element of L1();
consider y1 be Element of L1() such that
A10: y1 >= z1 and
A11: y1 in union S by A9,WAYBEL_0:def 15;
consider Z be set such that
A12: y1 in Z and
A13: Z in S by A11,TARSKI:def 4;
consider X1 be Subset of L1() such that
A14: Z = X1 and
A15: P[X1] by A1,A13;
A16: downarrow X1 in { downarrow X where X is Subset of L1() : P[X] } by A15;
z in downarrow X1 by A10,A12,A14,WAYBEL_0:def 15;
hence thesis by A16,TARSKI:def 4;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
registration
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
meet the set of all card B1 where B1 is with_bottom
CLbasis of L1 ;
coherence
proof
set X = the set of all card B2 where B2 is with_bottom CLbasis of L1 ;
defpred P[Ordinal] means $1 in the set of all
card B1 where B1 is with_bottom CLbasis of
L1;
A1: ex A be Ordinal st P[A]
proof
take card [#]L1;
[#]L1 is CLbasis of L1 by YELLOW15:25;
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 ORDINAL1:sch 1(A1);
ex B1 be with_bottom CLbasis of L1 st A = card B1 by A2;
then reconsider A as Cardinal;
A4: now
let x be object;
thus (for y be set holds y in X implies x in y) implies x in A by A2;
assume
A5: x in A;
let y be set;
assume
A6: y in X;
then ex B2 be with_bottom CLbasis of L1 st y = card B2;
then reconsider y1 = y as Cardinal;
A c= y1 by A3,A6;
hence x in y by A5;
end;
[#]L1 is CLbasis of L1 by YELLOW15:25;
then card [#]L1 in X;
hence thesis by A4,SETFAM_1:def 1;
end;
end;
theorem Th1:
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 the set of all card B2 where B2 is with_bottom CLbasis of L1 ;
hence thesis by SETFAM_1:3;
end;
theorem Th2:
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 the set of all
card B1 where B1 is with_bottom CLbasis of
L1;
set X = the set of all card B2 where B2 is with_bottom CLbasis of L1 ;
A1: ex A be Ordinal st P[A]
proof
take card [#]L1;
[#]L1 is CLbasis of L1 by YELLOW15:25;
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 ORDINAL1:sch 1(A1);
consider B1 be with_bottom CLbasis of L1 such that
A4: A = card B1 by A2;
A5: now
let x be object;
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 ex B2 be with_bottom CLbasis of L1 st y = card B2;
then reconsider y1 = y as Cardinal;
A c= y1 by A3,A7;
hence x in y by A6;
end;
take B1;
[#]L1 is CLbasis of L1 by YELLOW15:25;
then card [#]L1 in X;
hence thesis by A4,A5,SETFAM_1:def 1;
end;
theorem Th3: :: 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 = the set of all card B1 where B1 is with_bottom CLbasis of L1 ;
the carrier of CompactSublatt L1 is with_bottom CLbasis of L1 by WAYBEL23:71;
then
A1: card the carrier of CompactSublatt L1 in CB;
then
A2: meet CB c= card the carrier of CompactSublatt L1 by SETFAM_1:3;
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:71;
hence card the carrier of CompactSublatt L1 c= X by A3,CARD_1:11;
end;
then card the carrier of CompactSublatt L1 c= meet CB by A1,SETFAM_1:5;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Th4:
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 reconsider B2 = B1 as Subset-Family of T by XBOOLE_1:1;
A2: 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 A is open;
then A in the topology of T by PRE_TOPC:def 2;
then reconsider A1 = A as Element of L1 by A1,YELLOW_1:1;
let p be Point of T;
assume
A3: p in A;
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
A4: p in a and
A5: a in waybelow A1 /\ B1 by A3,TARSKI:def 4;
a in the carrier of L1 by A5;
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 A5,XBOOLE_0:def 4;
thus p in a by A4;
reconsider a1 = a as Element of L1 by A5;
a1 in waybelow A1 by A5,XBOOLE_0:def 4;
then a1 << A1 by WAYBEL_3:7;
then a1 <= A1 by WAYBEL_3:1;
hence thesis by A1,YELLOW_1:3;
end;
B2 c= the topology of T
proof
let x be object;
assume x in B2;
then reconsider x1 = x as Element of L1;
x1 in the carrier of L1;
hence thesis by A1,YELLOW_1:1;
end;
hence thesis by A2,YELLOW_9:32;
end;
theorem Th5:
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;
A3: 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;
y in the carrier of L1;
then
A4: 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 object such that
A5: v in y and
A6: not v in x;
v in y1 by A5;
then reconsider v as Point of T;
y1 is open by A4,PRE_TOPC:def 2;
then consider b be Subset of T such that
A7: b in B1 and
A8: v in b and
A9: b c= y1 by A5,YELLOW_9:31;
reconsider b as Element of L1 by A2,A7;
for z be object st z in {b} holds z in B2 by A2,A7,TARSKI:def 1;
then
A10: {b} is finite Subset of B2 by TARSKI:def 3;
take b;
ex_sup_of {b},L1 & b = "\/"({b},L1) by YELLOW_0:38,39;
then
b in { "\/"(Y,L1) where Y is finite Subset of B2: ex_sup_of Y,L1 } by A10;
hence b in finsups B2 by WAYBEL_0:def 27;
not b c= x by A6,A8;
hence not b <= x by A1,YELLOW_1:3;
thus thesis by A1,A9,YELLOW_1:3;
end;
now
let x,y be Element of L1;
assume that
A11: x in finsups B2 and
A12: y in finsups B2;
y in { "\/"(Y,L1) where Y is finite Subset of B2: ex_sup_of Y,L1 } by A12,
WAYBEL_0:def 27;
then consider Y2 be finite Subset of B2 such that
A13: y = "\/"(Y2,L1) and
A14: ex_sup_of Y2,L1;
x in { "\/"(Y,L1) where Y is finite Subset of B2: ex_sup_of Y,L1 } by A11,
WAYBEL_0:def 27;
then consider Y1 be finite Subset of B2 such that
A15: x = "\/"(Y1,L1) and
A16: ex_sup_of Y1,L1;
ex_sup_of (Y1 \/ Y2),L1 & "\/"(Y1 \/ Y2, L1) = "\/"(Y1, L1) "\/" "\/"
(Y2, L1) by A16,A14,YELLOW_2:3;
then
x "\/" y in { "\/" (Y,L1) where Y is finite Subset of B2: ex_sup_of Y
,L1 } by A15,A13;
then x "\/" y in finsups B2 by WAYBEL_0:def 27;
hence sup {x,y} in finsups B2 by YELLOW_0:41;
end;
then
A17: finsups B2 is join-closed by WAYBEL23:18;
{} c= B2 & ex_sup_of {},L1 by YELLOW_0:42;
then
"\/"({},L1) in {"\/"(Y,L1) where Y is finite Subset of B2: ex_sup_of Y, L1};
then Bottom L1 in finsups B2 by WAYBEL_0:def 27;
hence thesis by A17,A3,WAYBEL23:49,def 8;
end;
theorem Th6: :: 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: the set of all card B1 where B1 is Basis of T c= the set of all card B1
where B1 is with_bottom CLbasis of L1
proof
let b be object;
assume b in the set of all card B1 where B1 is Basis of T ;
then consider B2 be Basis of T such that
A4: b = card B2;
B2 c= the topology of T by TOPS_2:64;
then reconsider B3 = B2 as Subset of L1 by A1,YELLOW_1:1;
B2 is infinite by A2,YELLOW15:30;
then
A5: card B2 = card finsups B3 by YELLOW15:27;
finsups B3 is with_bottom CLbasis of L1 by A1,Th5;
hence thesis by A4,A5;
end;
the set of all card B1 where B1 is with_bottom CLbasis of L1
c= the set of all card B1 where B1 is Basis of T
proof
let b be object;
assume
b in the set of all card B1 where B1 is with_bottom CLbasis of L1 ;
then consider B2 be with_bottom CLbasis of L1 such that
A6: b = card B2;
B2 is Basis of T by A1,Th4;
hence thesis by A6;
end;
then the set of all card B1 where B1 is Basis of T = the set of all
card B1
where B1 is with_bottom CLbasis of L1 by A3,
XBOOLE_0:def 10;
hence thesis by WAYBEL23:def 5;
end;
theorem Th7: :: 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;
A1: card the carrier of T c= card the topology of T by YELLOW15:28;
assume InclPoset the topology of T = L1;
hence thesis by A1,YELLOW_1:1;
end;
theorem Th8: :: 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;
deffunc F(object) =
meet { A where A is Element of the topology of T : $1 in A };
A1: for x be object st x in the carrier of T holds F(x) in the carrier of
BoolePoset the carrier of T
proof
let x be object;
assume
A2: x in the carrier of T;
the carrier of T in the topology of T by PRE_TOPC:def 1;
then
the carrier of T in { A where A is Element of the topology of T : x in
A } by A2;
then meet { A where A is Element of the topology of T : x in A } c= the
carrier of T by SETFAM_1:3;
then meet { A where A is Element of the topology of T : x in A } in bool
the carrier of T;
hence thesis by WAYBEL_7:2;
end;
consider f be Function of the carrier of T, the carrier of BoolePoset the
carrier of T such that
A3: for x be object st x in the carrier of T holds f.x = F(x) from FUNCT_2:
sch 2 (A1);
reconsider rf = rng f as Subset-Family of T by WAYBEL_7:2;
A4: 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 A is open;
then
A5: A in the topology of T by PRE_TOPC:def 2;
let p be Point of T;
assume p in A;
then
A6: A in { C where C is Element of the topology of T : p in C } by A5;
meet { C where C is Element of the topology of T : p in C } c= the
carrier of T
proof
let z be object;
assume z in meet { C where C is Element of the topology of T : p in C };
then z in A by A6,SETFAM_1:def 1;
hence thesis;
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
A7: p in dom f by FUNCT_2:def 1;
a = f.p by A3;
hence a in rf by A7,FUNCT_1:def 3;
now
let Y be set;
assume Y in { C where C is Element of the topology of T : p in C };
then ex C be Element of the topology of T st Y = C & p in C;
hence p in Y;
end;
hence p in a by A6,SETFAM_1:def 1;
thus a c= A
by A6,SETFAM_1:def 1;
end;
assume
A8: T is finite;
rf c= the topology of T
proof
reconsider tT = the topology of T as finite non empty set by A8;
let z be object;
deffunc F(set) = $1;
assume z in rf;
then consider y be object such that
A9: y in dom f & z = f.y by FUNCT_1:def 3;
{ A where A is Element of the topology of T : y in A } c= bool the
carrier of T
proof
let z be object;
assume z in { A where A is Element of the topology of T : y in A };
then ex A be Element of the topology of T st z = A & y in A;
hence thesis;
end;
then reconsider
sfA = { A where A is Element of the topology of T : y in A } as
Subset-Family of T;
defpred P[set] means y in $1;
reconsider sfA as Subset-Family of T;
now
let P be Subset of T;
assume P in sfA;
then ex A be Element of the topology of T st P = A & y in A;
hence P is open by PRE_TOPC:def 2;
end;
then
A10: sfA is open by TOPS_2:def 1;
{F(A) where A is Element of tT: P[A]} is finite from PRE_CIRC:sch 1;
then
A11: meet sfA is open by A10,TOPS_2:20;
z = meet { A where A is Element of the topology of T : y in A } by A3,A9;
hence thesis by A11,PRE_TOPC:def 2;
end;
then rng f is Basis of T by A4,YELLOW_9:32;
then
A12: card rng f in the set of all card B1 where B1 is Basis of T ;
then
A13: meet the set of all card B1 where B1 is Basis of T c= card rng
f by SETFAM_1:3;
now
let x1,x2 be object;
assume that
A14: x1 in dom f & x2 in dom f and
A15: f.x1 = f.x2;
reconsider x3 = x1, x4 = x2 as Point of T by A14;
assume x1 <> x2;
then consider V be Subset of T such that
A16: V is open and
A17: x3 in V & not x4 in V or x4 in V & not x3 in V by T_0TOPSP:def 7;
A18: f.x3 = meet { A where A is Element of the topology of T : x3 in A } &
f.x4 = meet { A where A is Element of the topology of T : x4 in A } by A3;
now
per cases by A17;
suppose
A19: x3 in V & not x4 in V;
V in the topology of T by A16,PRE_TOPC:def 2;
then
A20: V in { A where A is Element of the topology of T : x3 in A } by A19;
A21: meet { A where A is Element of the topology of T : x3 in A } c= V
by A20,SETFAM_1:def 1;
A22: now
let Y be set;
assume Y in { A where A is Element of the topology of T : x4 in A };
then ex A be Element of the topology of T st Y = A & x4 in A;
hence x4 in Y;
end;
the carrier of T in the topology of T by PRE_TOPC:def 1;
then
the carrier of T in { A where A is Element of the topology of T :
x4 in A };
then x4 in meet { A where A is Element of the topology of T : x3 in A
} by A15,A18,A22,SETFAM_1:def 1;
hence contradiction by A19,A21;
end;
suppose
A23: x4 in V & not x3 in V;
V in the topology of T by A16,PRE_TOPC:def 2;
then
A24: V in { A where A is Element of the topology of T : x4 in A } by A23;
A25: meet { A where A is Element of the topology of T : x4 in A } c= V
by A24,SETFAM_1:def 1;
A26: now
let Y be set;
assume Y in { A where A is Element of the topology of T : x3 in A };
then ex A be Element of the topology of T st Y = A & x3 in A;
hence x3 in Y;
end;
the carrier of T in the topology of T by PRE_TOPC:def 1;
then
the carrier of T in { A where A is Element of the topology of T :
x3 in A };
then x3 in meet { A where A is Element of the topology of T : x4 in A
} by A15,A18,A26,SETFAM_1:def 1;
hence contradiction by A23,A25;
end;
end;
hence contradiction;
end;
then dom f = the carrier of T & f is one-to-one by FUNCT_1:def 4
,FUNCT_2:def 1;
then
A27: the carrier of T,rng f are_equipotent by WELLORD2:def 4;
for X be set st X in the set of all card B1 where B1 is Basis of T
holds card rng f c= X
proof
let X be set;
assume X in the set of all card B1 where B1 is Basis of T ;
then consider B2 be Basis of T such that
A28: X = card B2;
rng f c= B2
proof
let y be object;
assume y in rng f;
then consider x be object such that
A29: x in dom f and
A30: y = f.x by FUNCT_1:def 3;
reconsider x1 = x as Element of T by A29;
y = meet{ A where A is Element of the topology of T : x1 in A } by A3,A30
;
hence thesis by A8,YELLOW15:31;
end;
hence thesis by A28,CARD_1:11;
end;
then
card rng f c= meet the set of all card B1 where B1 is Basis of T
by A12,SETFAM_1:5;
then card rng f = meet the set of all card B1 where B1 is Basis of T
by A13,XBOOLE_0:def 10
.= weight T by WAYBEL23:def 5;
hence thesis by A27,CARD_1:5;
end;
theorem Th9: :: 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;
[#]L1 is with_bottom CLbasis of L1 by YELLOW15:25;
then
A2: card the carrier of L1 in the set of all
card B1 where B1 is with_bottom CLbasis of
L1;
A3: CLweight L1 c= card the carrier of L1
by A2,SETFAM_1:def 1;
assume
A4: T is finite;
now
let Z be set;
assume
Z in the set of all card B1 where B1 is with_bottom CLbasis of L1 ;
then consider B1 be with_bottom CLbasis of L1 such that
A5: Z = card B1;
Bottom L1 in B1 by WAYBEL23:def 8;
then the carrier of CompactSublatt L1 c= B1 by WAYBEL23:48;
then
A6: card the carrier of CompactSublatt L1 c= card B1 by CARD_1:11;
L1 is finite by A1,A4,YELLOW_1:1;
hence card the carrier of L1 c= Z by A5,A6,YELLOW15:26;
end;
then card the carrier of L1 c= meet the set of all
card B1 where B1 is with_bottom
CLbasis of L1 by A2,SETFAM_1:5;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th10:
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 object;
assume z in { uparrow V where V is Subset of T2 : V in B2 };
then ex V be Subset of T2 st z = uparrow V & V in B2;
hence thesis by A1;
end;
then reconsider upV = { uparrow V where V is Subset of T2 : V in B2 } as
Subset-Family of T1;
reconsider upV as Subset-Family of T1;
A2: the topology of T1 c= UniCl upV
proof
let z be object;
assume
A3: z in the topology of T1;
then reconsider z2 = z as Subset of T1;
z2 is open by A3,PRE_TOPC:def 2;
then z2 is upper by WAYBEL11:def 4;
then
A4: uparrow z2 c= z2 by WAYBEL_0:24;
reconsider z1 = z as Subset of T2 by A1,A3;
z in sigma T1 by A3,WAYBEL14:23;
then sigma T2 c= lambda T2 & z in sigma T2 by A1,WAYBEL30:10,YELLOW_9:52;
then z in lambda T2;
then z in the topology of T2 by WAYBEL30:9;
then
A5: z1 is open by PRE_TOPC:def 2;
{ uparrow G where G is Subset of T2 : G in B2 & G c= z1 } c= bool the
carrier of T1
proof
let v be object;
assume v in { uparrow G where G is Subset of T2 : G in B2 & G c= z1 };
then ex G be Subset of T2 st v = uparrow G & G in B2 & G c= z1;
hence thesis by A1;
end;
then reconsider
Y = { uparrow G where G is Subset of T2 : G in B2 & G c= z1 }
as Subset-Family of T1;
{ G where G is Subset of T2 : G in B2 & G c= z1 } c= bool the carrier of T1
proof
let v be object;
assume v in { G where G is Subset of T2 : G in B2 & G c= z1 };
then ex G be Subset of T2 st v = G & G in B2 & G c= z1;
hence thesis by A1;
end;
then reconsider Y1 = { G where G is Subset of T2 : G in B2 & G c= z1 } as
Subset-Family of T1;
defpred P[set] means $1 in B2 & $1 c= z1;
reconsider Y as Subset-Family of T1;
reconsider Y1 as Subset-Family of T1;
reconsider Y3 = Y1 as Subset-Family of T2 by A1;
A6: Y c= upV
proof
let v be object;
assume v in Y;
then ex G be Subset of T2 st v = uparrow G & G in B2 & G c= z1;
hence thesis;
end;
A7: 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 z1 = uparrow z2 by A4,XBOOLE_0:def 10
.= uparrow union Y1 by A5,YELLOW_8:9
.= uparrow union Y3 by A1,WAYBEL_0:13
.= union Y by A7;
hence thesis by A6,CANTOR_1:def 1;
end;
upV c= the topology of T1
proof
let z be object;
assume z in upV;
then consider V be Subset of T2 such that
A8: z = uparrow V and
A9: V in B2;
A10: T1 is Scott TopAugmentation of T2 by A1,YELLOW_9:def 4;
B2 c= the topology of T2 by TOPS_2:64;
then V in the topology of T2 by A9;
then V in lambda T2 by WAYBEL30:9;
then uparrow V in sigma T1 by A10,WAYBEL30:14;
hence thesis by A8,WAYBEL14:23;
end;
hence thesis by A2,CANTOR_1:def 2,TOPS_2:64;
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 WAYBEL23:74;
defpred P[object,object] means
ex y be Subset of T2 st y = $1 & $2 = uparrow y;
A2: for x be object st x in B1 ex z be object st P[x,z]
proof
let x be object;
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
A3: dom f = B1 and
A4: for x be object st x in B1 holds P[x,f.x] from CLASSES1:sch 1(A2);
{ uparrow V where V is Subset of T2 : V in B1 } c= rng f
proof
let z be object;
assume z in { uparrow V where V is Subset of T2 : V in B1 };
then consider V be Subset of T2 such that
A5: z = uparrow V and
A6: V in B1;
ex V1 be Subset of T2 st V1 = V & f.V = uparrow V1 by A4,A6;
hence thesis by A3,A5,A6,FUNCT_1:def 3;
end;
then
A7: card { uparrow V where V is Subset of T2 : V in B1 } c= card B1 by A3,
CARD_1:12;
{ uparrow V where V is Subset of T2 : V in B1 } is Basis of T1 by Th10;
then card { uparrow V where V is Subset of T2 : V in B1 } in the set of all
card B2 where
B2 is Basis of T1 ;
then meet the set of all card B2 where B2 is Basis of T1 c= card {
uparrow V where V is Subset of T2 : V in B1 } by SETFAM_1:3;
then meet the set of all card B2 where B2 is Basis of T1 c= card B1
by A7;
hence thesis by A1,WAYBEL23:def 5;
end;
theorem Th11:
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;
A2: x <= x;
x is compact by A1,WAYBEL_3:17;
hence thesis by A2;
end;
theorem Th12:
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;
A1: for y be Element of L1 st y is_>=_than compactbelow x holds x <= y
by Th11,LATTICE3:def 9;
for y be Element of L1 st y in compactbelow x holds y <= x by WAYBEL_8:4;
then x is_>=_than compactbelow x by LATTICE3:def 9;
hence thesis 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 thesis by YELLOW_0:40;
end;
end;
registration
cluster finite -> arithmetic for LATTICE;
coherence by Th12;
end;
registration
cluster reflexive transitive antisymmetric with_suprema with_infima
lower-bounded 1-element finite strict for RelStr;
existence
proof
0 in {0} by TARSKI:def 1;
then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:3;
reconsider T = RelStr(#{0},r#) as non empty RelStr;
take T;
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 thesis by ORDERS_2:def 5;
end;
then reconsider T9 = T as 1-element reflexive RelStr;
reconsider T99 = T9 as LATTICE;
T9 is transitive;
hence T is transitive;
T9 is antisymmetric;
hence T is antisymmetric;
T9 is with_suprema;
hence T is with_suprema;
T9 is with_infima;
hence T is with_infima;
T99 is lower-bounded;
hence T is lower-bounded;
thus T is 1-element;
thus T is finite;
thus thesis;
end;
end;
theorem Th13:
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 Th3;
the carrier of CompactSublatt L1 c= B1 by WAYBEL23:71;
hence thesis by A1,CARD_2:102;
end;
assume B1 = the carrier of CompactSublatt L1;
hence thesis by Th3;
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
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;
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;
wayabove a c= uparrow A
proof
let z be object;
assume
A2: z in wayabove a;
then reconsider z1 = z as Element of L1;
a << z1 by A2,WAYBEL_3:8;
then a <= z1 by WAYBEL_3:1;
hence thesis by A1,WAYBEL_0:def 20;
end;
hence thesis by XBOOLE_1:37;
end;
theorem Th16:
for L1 be non empty finite reflexive transitive RelStr holds Ids L1 is finite
proof
deffunc F(set) = $1;
let L1 be non empty finite reflexive transitive RelStr;
reconsider Y = bool the carrier of L1 as finite non empty set;
A1: the set of all X where X is Ideal of L1 c= { X where X is
Element of Y : X is Ideal of L1 }
proof
let z be object;
assume z in the set of all X where X is Ideal of L1 ;
then ex X1 be Ideal of L1 st z = X1;
hence thesis;
end;
defpred P[set] means $1 is Ideal of L1;
A2: { X where X is Element of Y : X is Ideal of L1 } c= the set of all
X where X is Ideal
of L1
proof
let z be object;
assume z in { X where X is Element of Y : X is Ideal of L1 };
then ex X1 be Element of Y st z = X1 & X1 is Ideal of L1;
hence thesis;
end;
A3: {F(X) where X is Element of Y : P[X]} is finite from PRE_CIRC:sch 1;
Ids L1 = the set of all X where X is Ideal of L1 by WAYBEL_0:def 23
.= { X where X is Element of Y : X is Ideal of L1 } by A1,A2,
XBOOLE_0:def 10;
hence thesis by A3;
end;
theorem Th17:
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
A1: L1 is infinite;
let B1 be with_bottom CLbasis of L1;
dom supMap subrelstr B1 = Ids subrelstr B1 & rng supMap subrelstr B1 =
the carrier of L1 by WAYBEL23:51,65;
then card the carrier of L1 c= card Ids subrelstr B1 by CARD_1:12;
then Ids subrelstr B1 is infinite by A1;
then subrelstr B1 is infinite by Th16;
hence thesis by YELLOW_0:def 15;
end;
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:22;
x <= inf wayabove x by WAYBEL14:9;
hence thesis by A1,YELLOW_0:def 3;
end;
theorem Th19:
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 object such that
A2: a1 in B1 by XBOOLE_0:def 1;
reconsider a1 as Element of L1 by A2;
{}(L1) c= B1;
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
WU = { 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;
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);
A3: for x be Element of B1* ex u be Element of WU st P[x,u]
proof
let x be Element of B1*;
reconsider y = x/.1 as Element of L1 by TARSKI:def 3;
rng Del(x,1) c= rng x by FINSEQ_3:106;
then
A4: rng Del(x,1) c= B1 by XBOOLE_1:1;
then reconsider z = rng Del(x,1) as Subset of L1 by XBOOLE_1:1;
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 A4;
then reconsider u = Way_Up(y,z) as Element of WU;
take u,y,z;
thus thesis;
end;
consider f be Function of B1*,WU such that
A5: for x be Element of B1* holds P[x,f.x] from FUNCT_2:sch 3(A3);
A6: dom f = B1* by FUNCT_2:def 1;
A7: WU c= rng f
proof
let z be object;
assume z in WU;
then consider a be Element of L1, A be finite Subset of L1 such that
A8: z = Way_Up(a,A) and
A9: a in B1 and
A10: A c= B1;
reconsider a1 = a as Element of B1 by A9;
consider p be FinSequence such that
A11: A = rng p by FINSEQ_1:52;
reconsider p as FinSequence of B1 by A10,A11,FINSEQ_1:def 4;
set q = <*a1*>^p;
A12: q in B1* by FINSEQ_1:def 11;
then consider y be Element of L1, v be Subset of L1 such that
A13: y = q/.1 and
A14: v = rng Del(q,1) and
A15: f.q = Way_Up(y,v) by A5;
A16: a = y by A13,FINSEQ_5:15;
A = v by A11,A14,WSIERP_1:40;
hence thesis by A6,A8,A12,A15,A16,FUNCT_1:def 3;
end;
B1 is infinite by A1,Th17;
then card B1 = card (B1*) by CARD_4:24;
hence thesis by A6,A7,CARD_1:12;
end;
theorem Th20:
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;
deffunc F(Element of T) = uparrow $1;
{ uparrow x where x is Element of T : x in X } c= bool the carrier of T
proof
let z be object;
assume z in { uparrow x where x is Element of T : x in X };
then ex x be Element of T st z = uparrow x & x in X;
hence thesis;
end;
then reconsider upx = { uparrow x where x is Element of T : x in X } 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 object;
assume z in { downarrow x where x is Element of T : x in X };
then ex x be Element of T st z = downarrow x & x in X;
hence thesis;
end;
then reconsider dox = { downarrow x where x is Element of T : x in X } as
Subset-Family of T;
reconsider dox as Subset-Family of T;
reconsider upx as Subset-Family of T;
A1: uparrow X = union upx by YELLOW_9:4;
now
let P be Subset of T;
assume P in upx;
then ex x be Element of T st P = uparrow x & x in X;
hence P is closed by WAYBEL19:38;
end;
then
A2: upx is closed by TOPS_2:def 2;
A3: X is finite;
{F(x) where x is Element of T : x in X } is finite from FRAENKEL:sch 21
(A3);
then uparrow X is closed by A2,A1,TOPS_2:21;
hence (uparrow X)` is open by TOPS_1:3;
deffunc F(Element of T) = downarrow $1;
A4: downarrow X = union dox by YELLOW_9:4;
now
let P be Subset of T;
assume P in dox;
then ex x be Element of T st P = downarrow x & x in X;
hence P is closed by WAYBEL19:38;
end;
then
A5: dox is closed by TOPS_2:def 2;
{F(x) where x is Element of T : x in X } is finite from FRAENKEL:sch 21
(A3);
then downarrow X is closed by A5,A4,TOPS_2:21;
hence thesis by TOPS_1:3;
end;
theorem Th21:
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 object;
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
ex a be Element of L1, A be finite Subset of L1 st z = Way_Up(a,A) & a
in B1 & A c= B1;
hence thesis by A1;
end;
then reconsider
WU = { 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;
reconsider WU as Subset-Family of T;
A2: now
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;
set S = the Scott TopAugmentation of T;
let A be Subset of T;
assume
A3: A is open;
let pT be Point of T;
assume pT in A;
then consider a be Subset of T such that
A4: a in BL and
A5: pT in a and
A6: a c= A by A3,YELLOW_9:31;
consider W,FT be Subset of T such that
A7: a = W \ uparrow FT and
A8: W in sigma T and
A9: FT is finite by A4;
A10: the RelStr of S = the RelStr of T by YELLOW_9:def 4;
then reconsider pS = pT as Element of S;
reconsider W1 = W as Subset of S by A10;
sigma S = sigma T by A10,YELLOW_9:52;
then
A11: W = union { wayabove x where x is Element of S : x in W1 } by A8,
WAYBEL14:33;
reconsider pL = pS as Element of L1 by A1;
defpred P[object,object] means
ex b1,y1 be Element of L1 st y1 = $1 & b1 = $2 &
b1 in B1 & not b1 <= pL & b1 << y1;
A12: Bottom L1 in B1 by WAYBEL23:def 8;
pT in W by A5,A7,XBOOLE_0:def 5;
then consider k be set such that
A13: pT in k and
A14: k in { wayabove x where x is Element of S : x in W1 } by A11,TARSKI:def 4;
consider xS be Element of S such that
A15: k = wayabove xS and
A16: xS in W1 by A14;
reconsider xL = xS as Element of L1 by A1,A10;
xS << pS by A13,A15,WAYBEL_3:8;
then xL << pL by A1,A10,WAYBEL_8:8;
then consider bL be Element of L1 such that
A17: bL in B1 and
A18: xL <= bL and
A19: bL << pL by A12,WAYBEL23:47;
reconsider FL = FT as Subset of L1 by A1;
A20: uparrow FT = uparrow FL by A1,WAYBEL_0:13;
A21: not pT in uparrow FT by A5,A7,XBOOLE_0:def 5;
A22: for y be object st y in FL ex b be object st P[y,b]
proof
let y be object;
assume
A23: y in FL;
then reconsider y1 = y as Element of L1;
not y1 <= pL by A21,A20,A23,WAYBEL_0:def 16;
then consider b1 be Element of L1 such that
A24: b1 in B1 & not b1 <= pL & b1 << y1 by WAYBEL23:46;
reconsider b = b1 as set;
take b,b1,y1;
thus thesis by A24;
end;
consider f be Function such that
A25: dom f = FL and
A26: for y be object st y in FL holds P[y,f.y] from CLASSES1:sch 1(A22);
rng f c= the carrier of L1
proof
let z be object;
assume z in rng f;
then consider v be object such that
A27: v in dom f and
A28: z = f.v by FUNCT_1:def 3;
ex b1,y1 be Element of L1 st y1 = v & b1 = f.v & b1 in B1 &( not b1
<= pL)& b1 << y1 by A25,A26,A27;
hence thesis by A28;
end;
then reconsider FFL = rng f as Subset of L1;
A29: FFL c= B1
proof
let z be object;
assume z in FFL;
then consider v be object such that
A30: v in dom f and
A31: z = f.v by FUNCT_1:def 3;
ex b1,y1 be Element of L1 st y1 = v & b1 = f.v & b1 in B1 &( not b1
<= pL)& b1 << y1 by A25,A26,A30;
hence thesis by A31;
end;
A32: uparrow FL c= uparrow FFL
proof
let z be object;
assume
A33: z in uparrow FL;
then reconsider z1 = z as Element of L1;
consider v1 be Element of L1 such that
A34: v1 <= z1 and
A35: v1 in FL by A33,WAYBEL_0:def 16;
consider b1,y1 be Element of L1 such that
A36: y1 = v1 and
A37: b1 = f.v1 and
b1 in B1 and
not b1 <= pL and
A38: b1 << y1 by A26,A35;
b1 << z1 by A34,A36,A38,WAYBEL_3:2;
then
A39: b1 <= z1 by WAYBEL_3:1;
b1 in FFL by A25,A35,A37,FUNCT_1:def 3;
hence thesis by A39,WAYBEL_0:def 16;
end;
reconsider cT = wayabove bL \ uparrow FFL as Subset of T by A1;
take cT;
cT = Way_Up(bL,FFL) & FFL is finite by A9,A25,FINSET_1:8;
hence cT in WU by A17,A29;
wayabove bL c= wayabove xL by A18,WAYBEL_3:12;
then
A40: wayabove bL \ uparrow FFL c= wayabove xL \ uparrow FL by A32,XBOOLE_1:35;
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 object such that
A41: v in dom f and
A42: z = f.v by FUNCT_1:def 3;
ex b1,y1 be Element of L1 st y1 = v & b1 = f.v & b1 in B1 &( not b1
<= pL)& b1 << y1 by A25,A26,A41;
hence thesis by A42;
end;
then for z be Element of L1 holds not z <= pL or not z in FFL;
then
A43: not pL in uparrow FFL by WAYBEL_0:def 16;
pL in wayabove bL by A19,WAYBEL_3:8;
hence pT in cT by A43,XBOOLE_0:def 5;
wayabove xL c= W
proof
let z be object;
wayabove xL = wayabove xS by A1,A10,YELLOW12:13;
then
A44: wayabove xL in { wayabove x where x is Element of S : x in W1 } by A16;
assume z in wayabove xL;
hence thesis by A11,A44,TARSKI:def 4;
end;
then wayabove xL \ uparrow FL c= a by A7,A20,XBOOLE_1:33;
then wayabove bL \ uparrow FFL c= a by A40;
hence cT c= A by A6;
end;
WU c= the topology of T
proof
let z be object;
assume z in WU;
then consider a be Element of L1, A be finite Subset of L1 such that
A45: z = Way_Up(a,A) and
a in B1 and
A c= B1;
reconsider A1 = A as finite Subset of T by A1;
reconsider a1 = a as Element of T by A1;
wayabove a1 is open & (uparrow A1)` is open by Th20,WAYBEL19:40;
then
A46: wayabove a1 /\ (uparrow A1)` is open by TOPS_1:11;
z = wayabove a1 \ uparrow A by A1,A45,YELLOW12:13
.= wayabove a1 \ uparrow A1 by A1,WAYBEL_0:13
.= wayabove a1 /\ (uparrow A1)` by SUBSET_1:13;
hence thesis by A46,PRE_TOPC:def 2;
end;
hence thesis by A2,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;
consider B1 be with_bottom CLbasis of L1 such that
A1: card B1 = CLweight L1 by Th2;
A2: the RelStr of T = the RelStr of L1 by YELLOW_9:def 4;
now
per cases;
suppose
A3: L1 is finite;
then
A4: T is finite by A2;
B1 = the carrier of CompactSublatt L1 by A1,A3,Th13
.= the carrier of L1 by A3,YELLOW15:26;
hence thesis by A2,A1,A4,Th8;
end;
suppose
A5: L1 is infinite;
set WU = { Way_Up(a,A) where a is Element of L1, A is finite Subset of
L1: a in B1 & A c= B1 };
WU is Basis of T by Th21;
then
A6: weight T c= card WU by WAYBEL23:73;
card WU c= CLweight L1 by A1,A5,Th19;
hence thesis by A6;
end;
end;
hence thesis;
end;
theorem Th22:
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;
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 object;
assume z in b2;
then ex u be Subset of T st z = wayabove inf u & u in b;
hence thesis;
end;
then reconsider b2 as Subset-Family of T;
reconsider b1 = the set of all wayabove x where x is Element of T as
Basis of T by WAYBEL11:45;
A1: now
let A be Subset of T;
assume
A2: A is open;
let a be Point of T;
assume a in A;
then consider C be Subset of T such that
A3: C in b1 and
A4: a in C and
A5: C c= A by A2,YELLOW_9:31;
C is open by A3,YELLOW_8:10;
then consider D be Subset of T such that
A6: D in b and
A7: a in D and
A8: D c= C by A4,YELLOW_9:31;
D is open by A6,YELLOW_8:10;
then consider E be Subset of T such that
A9: E in b1 and
A10: a in E and
A11: E c= D by A7,YELLOW_9:31;
consider z be Element of T such that
A12: E = wayabove z by A9;
take u = wayabove inf D;
thus u in b2 by A6;
reconsider a1 = a as Element of T;
consider x be Element of T such that
A13: C = wayabove x by A3;
z << a1 by A10,A12,WAYBEL_3:8;
then consider y be Element of T such that
A14: z << y and
A15: y << a1 by WAYBEL_4:52;
inf D is_<=_than D & y in wayabove z by A14,WAYBEL_3:8,YELLOW_0:33;
then inf D <= y by A11,A12,LATTICE3:def 8;
then inf D << a1 by A15,WAYBEL_3:2;
hence a in u by WAYBEL_3:8;
A16: wayabove x c= uparrow x by WAYBEL_3:11;
ex_inf_of uparrow x,T & ex_inf_of D,T by YELLOW_0:17;
then inf uparrow x <= inf D by A13,A8,A16,XBOOLE_1:1,YELLOW_0:35;
then x <= inf D by WAYBEL_0:39;
then wayabove inf D c= C by A13,WAYBEL_3:12;
hence u c= A by A5;
end;
b2 c= the topology of T
proof
let z be object;
assume z in b2;
then consider u be Subset of T such that
A17: z = wayabove inf u and
u in b;
wayabove inf u is open by WAYBEL11:36;
hence thesis by A17,PRE_TOPC:def 2;
end;
hence thesis by A1,YELLOW_9:32;
end;
theorem Th23:
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;
reconsider B2 = { inf u where u is Subset of T : u in B1 } as set;
defpred P[object,object] means
ex y be Element of T st $1 = y & $2 = wayabove y;
reconsider B3 = { wayabove inf u where u is Subset of T : u in B1 } as Basis
of T by Th22;
assume that
A1: B1 is infinite and
A2: { inf u where u is Subset of T : u in B1 } is finite;
A3: for x be object st x in B2 ex y be object st y in B3 & P[x,y]
proof
let x be object;
assume x in B2;
then
A4: ex u1 be Subset of T st x = inf u1 & u1 in B1;
then reconsider z = x as Element of T;
take y = wayabove z;
thus y in B3 by A4;
take z;
thus thesis;
end;
consider f be Function such that
A5: dom f = B2 and
A6: rng f c= B3 and
A7: for x be object st x in B2 holds P[x,f.x] from FUNCT_1:sch 6(A3);
B3 c= rng f
proof
let z be object;
assume z in B3;
then consider u1 be Subset of T such that
A8: z = wayabove inf u1 and
A9: u1 in B1;
inf u1 in B2 by A9;
then
A10: ex y be Element of T st inf u1 = y & f.(inf u1) = wayabove y by A7;
inf u1 in B2 by A9;
hence thesis by A5,A8,A10,FUNCT_1:def 3;
end;
then rng f = B3 by A6,XBOOLE_0:def 10;
then B3 is finite by A2,A5,FINSET_1:8;
then T is finite by YELLOW15:30;
hence contradiction by A1;
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 WAYBEL23:74;
{ inf u where u is Subset of T : u in B1 } c= the carrier of T
proof
let z be object;
assume z in { inf u where u is Subset of T : u in B1 };
then ex u be Subset of T st z = inf u & u in B1;
hence thesis;
end;
then reconsider
B0 = { inf u where u is Subset of T : u in B1 } as Subset of T;
set B2 = finsups B0;
defpred P[object,object] means
ex y be Subset of T st $1 = y & $2 = inf y;
A2: for x be object st x in B1 ex y be object st y in B0 & P[x,y]
proof
let x be object;
assume
A3: x in B1;
then reconsider z = x as Subset of T;
take y = inf z;
thus y in B0 by A3;
take z;
thus thesis;
end;
consider f be Function such that
A4: dom f = B1 and
rng f c= B0 and
A5: for x be object st x in B1 holds P[x,f.x] from FUNCT_1:sch 6(A2);
B0 c= rng f
proof
let z be object;
assume z in B0;
then consider u be Subset of T such that
A6: z = inf u and
A7: u in B1;
ex y be Subset of T st u = y & f.u = inf y by A5,A7;
hence thesis by A4,A6,A7,FUNCT_1:def 3;
end;
then
A8: card B0 c= card B1 by A4,CARD_1:12;
A9: the RelStr of L1 = the RelStr of T by YELLOW_9:def 4;
A10: now
per cases;
suppose
A11: L1 is finite;
the carrier of L1 c= B0
proof
let z be object;
assume z in the carrier of L1;
then reconsider z1 = z as Element of T by A9;
z1 <= z1;
then
A12: z1 in uparrow z1 by WAYBEL_0:18;
T is finite by A9,A11;
then uparrow z1 is open by WAYBEL11:def 5;
then consider A be Subset of T such that
A13: A in B1 and
A14: z1 in A and
A15: A c= uparrow z1 by A12,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 A15,YELLOW_0:35;
then
A16: z1 <= inf A by WAYBEL_0:39;
inf A <= z1 by A14,YELLOW_2:22;
then z = inf A by A16,YELLOW_0:def 3;
hence thesis by A13;
end;
then B0 c= B2 & B2 c= B0 by A9,WAYBEL_0:50;
hence card B2 = card B0 by XBOOLE_0:def 10;
end;
suppose
L1 is infinite;
then T is infinite by A9;
then B0 is infinite by Th23,YELLOW15:30;
hence card B2 = card B0 by YELLOW15:27;
end;
end;
ex_sup_of {},T & {} is finite Subset of B0 by XBOOLE_1:2,YELLOW_0:42;
then
"\/"({},T) in {"\/" (Y,T) where Y is finite Subset of B0: ex_sup_of Y,T };
then "\/"({},T) in finsups B0 by WAYBEL_0:def 27;
then
A17: Bottom L1 in B2 by A9,YELLOW_0:26,42;
reconsider B2 as Subset of L1 by A9;
now
let x,y be Element of L1;
assume that
A18: x in B2 and
A19: y in B2;
y in { "\/"(Y,T) where Y is finite Subset of B0 : ex_sup_of Y,T } by A19,
WAYBEL_0:def 27;
then consider Y2 be finite Subset of B0 such that
A20: y = "\/"(Y2,T) and
A21: ex_sup_of Y2,T;
x in { "\/"(Y,T) where Y is finite Subset of B0 : ex_sup_of Y,T } by A18,
WAYBEL_0:def 27;
then consider Y1 be finite Subset of B0 such that
A22: x = "\/"(Y1,T) and
A23: ex_sup_of Y1,T;
A24: ex_sup_of Y1 \/ Y2,T by YELLOW_0:17;
sup {x,y} = x "\/" y by YELLOW_0:41
.= "\/"(Y1,T) "\/" "\/"(Y2,T) by A9,A22,A20,YELLOW12:10
.= "\/"(Y1 \/ Y2,T) by A23,A21,YELLOW_2:3;
then
sup {x,y} in { "\/"(Y,T) where Y is finite Subset of B0 : ex_sup_of Y
,T } by A24;
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 A9;
A25: B0 c= B2 by WAYBEL_0:50;
assume x << y;
then y in wayabove x by WAYBEL_3:8;
then
A26: y1 in wayabove x1 by A9,YELLOW12:13;
wayabove x1 is open by WAYBEL11:36;
then consider u be Subset of T such that
A27: u in B1 and
A28: y1 in u and
A29: u c= wayabove x1 by A26,YELLOW_9:31;
reconsider b = inf u as Element of L1 by A9;
take b;
b in B0 by A27;
hence b in B2 by A25;
A30: wayabove x1 c= uparrow x1 by WAYBEL_3:11;
ex_inf_of uparrow x1,T & ex_inf_of u,T by YELLOW_0:17;
then inf uparrow x1 <= inf u by A29,A30,XBOOLE_1:1,YELLOW_0:35;
then x1 <= inf u by WAYBEL_0:39;
hence x <= b by A9,YELLOW_0:1;
u is open by A27,YELLOW_8:10;
hence thesis by A9,A28,WAYBEL14:26,WAYBEL_8:8;
end;
then
A31: B2 is CLbasis of L1 by A17,WAYBEL23:47;
B2 is with_bottom by A17,WAYBEL23:def 8;
then CLweight L1 c= card B0 by A10,A31,Th1;
hence thesis by A1,A8;
end;
theorem Th24: :: 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;
set T1 = the Lawson correct TopAugmentation of L1;
weight T c= weight T1 & weight T1 c= CLweight L1 by Lm1,Lm2;
then
A1: weight T c= CLweight L1;
CLweight L1 c= weight T by Lm3;
hence thesis 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;
set T1 = the Scott TopAugmentation of L1;
CLweight L1 c= weight T1 & weight T1 c= weight T by Lm1,Lm3;
then
A1: CLweight L1 c= weight T;
weight T c= CLweight L1 by Lm2;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th26:
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 Function 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:5;
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;
A2: card the carrier of CompactSublatt InclPoset Ids subrelstr B1 = card the
carrier of subrelstr B1 by Th26,WAYBEL23:69;
thus CLweight InclPoset Ids subrelstr B1 = card the carrier of
CompactSublatt InclPoset Ids subrelstr B1 by Th3
.= CLweight L1 by A1,A2,YELLOW_0:def 15;
end;
registration
let L1 be continuous lower-bounded sup-Semilattice;
cluster InclPoset sigma L1 -> with_suprema continuous;
coherence
proof
set S = the 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;
set S = the Scott TopAugmentation of L1;
A1: the RelStr of S = the RelStr of L1 by YELLOW_9:def 4;
A2: InclPoset the topology of S = InclPoset sigma L1 by YELLOW_9:51;
A3: CLweight L1 = weight S by Th24;
now
per cases;
suppose
L1 is infinite;
then S is infinite by A1;
hence thesis by A3,A2,Th6;
end;
suppose
A4: L1 is finite;
A5: card the carrier of S c= card the carrier of InclPoset sigma L1 by A2,Th7
;
A6: S is finite by A1,A4;
then weight S = card the carrier of S by Th8;
hence thesis by A3,A2,A6,A5,Th9;
end;
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;
set S = the Scott TopAugmentation of L1;
assume
A1: L1 is infinite;
A2: CLweight L1 = weight S & InclPoset the topology of S = InclPoset sigma
L1 by Th24,YELLOW_9:51;
the RelStr of S = the RelStr of L1 by YELLOW_9:def 4;
then S is infinite by A1;
hence thesis by A2,Th6;
end;