:: Weights of Continuous Lattices
:: by Robert Milewski
::
:: Copyright (c) 2000-2019 Association of Mizar Users

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 { () 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 { () 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 ()) -> algebraic ;
coherence
InclPoset (Ids ()) 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 Th1: :: WAYBEL31:1
for L1 being continuous sup-Semilattice
for B1 being with_bottom CLbasis of L1 holds CLweight L1 c= card B1
proof end;

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

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

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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

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
proof end;

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 { () 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 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
proof end;

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

registration
coherence
for b1 being LATTICE st b1 is finite holds
b1 is arithmetic
by Th12;
end;

registration
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 )
proof end;
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 () )
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
() \ ();
coherence
() \ () 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) = () \ ();

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) = {}
proof end;

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

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
proof end;

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

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
proof end;

theorem Th20: :: WAYBEL31:20
for T being complete Lawson TopLattice
for X being finite Subset of T holds
( ()  is open & ()  is open )
proof end;

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
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 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
proof end;

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
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 Th24: :: WAYBEL31:24
for L1 being lower-bounded continuous sup-Semilattice
for T being Scott TopAugmentation of L1 holds CLweight L1 = weight T
proof end;

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

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
proof end;

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 ()))
proof end;

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

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

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