:: Weights of Continuous Lattices
:: by Robert Milewski
::
:: Received January 6, 2000
:: Copyright (c) 2000-2012 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]  }
proofend;

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]  }
proofend;

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
proofend;
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 Th1: :: WAYBEL31:1
for L1 being continuous sup-Semilattice
for B1 being with_bottom CLbasis of L1 holds CLweight L1 c= card B1
proofend;

theorem Th2: :: WAYBEL31:2
for L1 being continuous sup-Semilattice ex B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1
proofend;

theorem Th3: :: WAYBEL31:3
for L1 being lower-bounded algebraic LATTICE holds CLweight L1 = card the carrier of (CompactSublatt L1)
proofend;

theorem Th4: :: WAYBEL31:4
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
proofend;

theorem Th5: :: WAYBEL31:5
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
proofend;

theorem Th6: :: WAYBEL31:6
for T being non empty T_0 TopSpace
for L1 being lower-bounded continuous sup-Semilattice st InclPoset the topology of T = L1 & T is infinite holds
weight T = CLweight L1
proofend;

theorem Th7: :: WAYBEL31:7
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
proofend;

theorem Th8: :: WAYBEL31:8
for T being non empty T_0 TopSpace st T is finite holds
weight T = card the carrier of T
proofend;

theorem Th9: :: WAYBEL31:9
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
proofend;

theorem Th10: :: WAYBEL31:10
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
proofend;

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
proofend;

theorem Th11: :: WAYBEL31:11
for L1 being non empty up-complete Poset st L1 is finite holds
for x being Element of L1 holds x in compactbelow x
proofend;

theorem Th12: :: WAYBEL31:12
for L1 being finite LATTICE holds L1 is arithmetic
proofend;

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

registration
cluster finite 1 -element strict reflexive transitive antisymmetric lower-bounded with_suprema with_infima for RelStr ;
existence
 ex b1 being RelStr st
( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is with_suprema & b1 is with_infima & b1 is lower-bounded & b1 is 1 -element & b1 is finite & b1 is strict )
proofend;
end;

theorem Th13: :: WAYBEL31:13
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) )
proofend;

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:14
for L1 being non empty reflexive RelStr
for a being Element of L1 holds Way_Up (a,({} L1)) = wayabove a ;

theorem :: WAYBEL31:15
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) = {}
proofend;

theorem Th16: :: WAYBEL31:16
for L1 being non empty finite reflexive transitive RelStr holds Ids L1 is finite
proofend;

theorem Th17: :: WAYBEL31:17
for L1 being lower-bounded continuous sup-Semilattice st L1 is infinite holds
for B1 being with_bottom CLbasis of L1 holds B1 is infinite
proofend;

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

theorem Th19: :: WAYBEL31:19
for L1 being lower-bounded continuous sup-Semilattice st L1 is infinite 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
proofend;

theorem Th20: :: WAYBEL31:20
for T being complete Lawson TopLattice
for X being finite Subset of T holds
( (uparrow X) ` is open & (downarrow X) ` is open )
proofend;

theorem Th21: :: WAYBEL31:21
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
proofend;

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

theorem Th22: :: WAYBEL31:22
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
proofend;

theorem Th23: :: WAYBEL31:23
for L1 being lower-bounded continuous sup-Semilattice
for T being Scott TopAugmentation of L1
for B1 being Basis of T st B1 is infinite holds
{  (inf u) where u is Subset of T : u in B1  }  is infinite
proofend;

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

theorem Th24: :: WAYBEL31:24
for L1 being lower-bounded continuous sup-Semilattice
for T being Scott TopAugmentation of L1 holds CLweight L1 = weight T
proofend;

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

theorem Th26: :: WAYBEL31:26
for L1, L2 being non empty RelStr st L1,L2 are_isomorphic holds
card the carrier of L1 = card the carrier of L2
proofend;

theorem :: WAYBEL31:27
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)))
proofend;

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 )
proofend;
end;

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

theorem :: WAYBEL31:29
for L1 being lower-bounded continuous sup-Semilattice st L1 is infinite holds
CLweight L1 = CLweight (InclPoset (sigma L1))
proofend;