:: Weights of Continuous Lattices
:: by Robert Milewski
::
:: Received January 6, 2000
:: Copyright (c) 2000-2011 Association of Mizar Users


begin

scheme :: WAYBEL31:sch 1
UparrowUnion{ F1() -> RelStr , P1[ set ] } :
for S being Subset-Family of F1() st S = { X where X is Subset of F1() : P1[X] } holds
uparrow (union S) = union { (uparrow X) where X is Subset of F1() : P1[X] }
proof end;

scheme :: WAYBEL31:sch 2
DownarrowUnion{ F1() -> RelStr , P1[ set ] } :
for S being Subset-Family of F1() st S = { X where X is Subset of F1() : P1[X] } holds
downarrow (union S) = union { (downarrow X) where X is Subset of F1() : P1[X] }
proof 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
InclPoset (Ids (subrelstr B1)) is algebraic
by WAYBEL13:10;
end;

definition
let L1 be continuous sup-Semilattice;
func CLweight L1 -> Cardinal equals :: WAYBEL31:def 1
meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;
coherence
meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } is Cardinal
proof end;
end;

:: deftheorem defines CLweight WAYBEL31:def 1 :
for L1 being continuous sup-Semilattice holds CLweight L1 = meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;

theorem :: WAYBEL31:1
canceled;

theorem :: WAYBEL31:2
canceled;

theorem Th3: :: WAYBEL31:3
for L1 being continuous sup-Semilattice
for B1 being with_bottom CLbasis of L1 holds CLweight L1 c= card B1
proof end;

theorem Th4: :: WAYBEL31:4
for L1 being continuous sup-Semilattice ex B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1
proof end;

theorem Th5: :: WAYBEL31:5
for L1 being lower-bounded algebraic LATTICE holds CLweight L1 = card the carrier of (CompactSublatt L1)
proof end;

theorem Th6: :: WAYBEL31:6
for T being non empty TopSpace
for L1 being continuous sup-Semilattice st InclPoset the topology of T = L1 holds
for B1 being with_bottom CLbasis of L1 holds B1 is Basis of T
proof end;

theorem Th7: :: WAYBEL31:7
for T being non empty TopSpace
for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 holds
for B1 being Basis of T
for B2 being Subset of L1 st B1 = B2 holds
finsups B2 is with_bottom CLbasis of L1
proof end;

theorem Th8: :: WAYBEL31:8
for T being non empty T_0 TopSpace
for L1 being lower-bounded continuous sup-Semilattice st InclPoset the topology of T = L1 & not T is finite holds
weight T = CLweight L1
proof end;

theorem Th9: :: WAYBEL31:9
for T being non empty T_0 TopSpace
for L1 being continuous sup-Semilattice st InclPoset the topology of T = L1 holds
card the carrier of T c= card the carrier of L1
proof end;

theorem Th10: :: WAYBEL31:10
for T being non empty T_0 TopSpace st T is finite holds
weight T = card the carrier of T
proof end;

theorem Th11: :: WAYBEL31:11
for T being TopStruct
for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 & T is finite holds
CLweight L1 = card the carrier of L1
proof end;

theorem Th12: :: WAYBEL31:12
for L1 being lower-bounded continuous sup-Semilattice
for T1 being Scott TopAugmentation of L1
for T2 being correct Lawson TopAugmentation of L1
for B2 being Basis of T2 holds { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1
proof end;

Lm1: for L1 being lower-bounded continuous sup-Semilattice
for T1 being Scott TopAugmentation of L1
for T2 being correct Lawson TopAugmentation of L1 holds weight T1 c= weight T2
proof end;

theorem :: WAYBEL31:13
canceled;

theorem Th14: :: WAYBEL31:14
for L1 being non empty up-complete Poset st L1 is finite holds
for x being Element of L1 holds x in compactbelow x
proof end;

theorem Th15: :: WAYBEL31:15
for L1 being finite LATTICE holds L1 is arithmetic
proof end;

registration
cluster finite reflexive transitive antisymmetric with_suprema with_infima -> arithmetic RelStr ;
coherence
for b1 being LATTICE st b1 is finite holds
b1 is arithmetic
by Th15;
end;

registration
cluster non empty trivial finite strict reflexive transitive antisymmetric lower-bounded with_suprema with_infima RelStr ;
existence
ex b1 being RelStr st
( b1 is trivial & b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is with_suprema & b1 is with_infima & b1 is lower-bounded & not b1 is empty & b1 is finite & b1 is strict )
proof end;
end;

theorem Th16: :: WAYBEL31:16
for L1 being finite LATTICE
for B1 being with_bottom CLbasis of L1 holds
( card B1 = CLweight L1 iff B1 = the carrier of (CompactSublatt L1) )
proof 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 :: WAYBEL31:def 2
(wayabove a) \ (uparrow A);
coherence
(wayabove a) \ (uparrow A) is Subset of L1
;
end;

:: deftheorem defines Way_Up WAYBEL31:def 2 :
for L1 being non empty reflexive RelStr
for A being Subset of L1
for a being Element of L1 holds Way_Up (a,A) = (wayabove a) \ (uparrow A);

theorem :: WAYBEL31:17
for L1 being non empty reflexive RelStr
for a being Element of L1 holds Way_Up (a,({} L1)) = wayabove a ;

theorem :: WAYBEL31:18
for L1 being non empty Poset
for A being Subset of L1
for a being Element of L1 st a in uparrow A holds
Way_Up (a,A) = {}
proof end;

theorem Th19: :: WAYBEL31:19
for L1 being non empty finite reflexive transitive RelStr holds Ids L1 is finite
proof end;

theorem Th20: :: WAYBEL31:20
for L1 being lower-bounded continuous sup-Semilattice st not L1 is finite holds
for B1 being with_bottom CLbasis of L1 holds not B1 is finite
proof end;

theorem :: WAYBEL31:21
canceled;

theorem :: WAYBEL31:22
canceled;

theorem :: WAYBEL31:23
for L1 being non empty complete Poset
for x being Element of L1 st x is compact holds
x = inf (wayabove x)
proof end;

theorem Th24: :: WAYBEL31:24
for L1 being lower-bounded continuous sup-Semilattice st not L1 is finite holds
for B1 being 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 end;

theorem Th25: :: WAYBEL31:25
for T being complete Lawson TopLattice
for X being finite Subset of T holds
( (uparrow X) ` is open & (downarrow X) ` is open )
proof end;

theorem Th26: :: WAYBEL31:26
for L1 being lower-bounded continuous sup-Semilattice
for T being correct Lawson TopAugmentation of L1
for B1 being 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 end;

Lm2: for L1 being lower-bounded continuous sup-Semilattice
for T being correct Lawson TopAugmentation of L1 holds weight T c= CLweight L1
proof end;

theorem Th27: :: WAYBEL31:27
for L1 being lower-bounded continuous sup-Semilattice
for T being Scott TopAugmentation of L1
for b being Basis of T holds { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T
proof end;

theorem Th28: :: WAYBEL31:28
for L1 being lower-bounded continuous sup-Semilattice
for T being Scott TopAugmentation of L1
for B1 being Basis of T st not B1 is finite holds
not { (inf u) where u is Subset of T : u in B1 } is finite
proof end;

Lm3: for L1 being lower-bounded continuous sup-Semilattice
for T being Scott TopAugmentation of L1 holds CLweight L1 c= weight T
proof end;

theorem Th29: :: WAYBEL31:29
for L1 being lower-bounded continuous sup-Semilattice
for T being Scott TopAugmentation of L1 holds CLweight L1 = weight T
proof end;

theorem :: WAYBEL31:30
for L1 being lower-bounded continuous sup-Semilattice
for T being correct Lawson TopAugmentation of L1 holds CLweight L1 = weight T
proof end;

theorem Th31: :: WAYBEL31:31
for L1, L2 being non empty RelStr st L1,L2 are_isomorphic holds
card the carrier of L1 = card the carrier of L2
proof end;

theorem :: WAYBEL31:32
for L1 being lower-bounded continuous sup-Semilattice
for B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1 holds
CLweight L1 = CLweight (InclPoset (Ids (subrelstr B1)))
proof end;

registration
let L1 be lower-bounded continuous sup-Semilattice;
cluster InclPoset (sigma L1) -> with_suprema continuous ;
coherence
( InclPoset (sigma L1) is with_suprema & InclPoset (sigma L1) is continuous )
proof end;
end;

theorem :: WAYBEL31:33
for L1 being lower-bounded continuous sup-Semilattice holds CLweight L1 c= CLweight (InclPoset (sigma L1))
proof end;

theorem :: WAYBEL31:34
for L1 being lower-bounded continuous sup-Semilattice st not L1 is finite holds
CLweight L1 = CLweight (InclPoset (sigma L1))
proof end;