:: 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{ F₁() -> RelStr , P₁[ set ] } :

for S being Subset-Family of F₁() st S = { X where X is Subset of F₁() : P₁[X] } holds
uparrow (union S) = union { (uparrow X) where X is Subset of F₁() : P₁[X] }

proof end;

scheme :: WAYBEL31:sch 2
DownarrowUnion{ F₁() -> RelStr , P₁[ set ] } :

for S being Subset-Family of F₁() st S = { X where X is Subset of F₁() : P₁[X] } holds
downarrow (union S) = union { (downarrow X) where X is Subset of F₁() : P₁[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 b₁ being LATTICE st b₁ is finite holds
b₁ is arithmetic by Th15;

end;

registration

cluster non empty trivial finite strict reflexive transitive antisymmetric lower-bounded with_suprema with_infima RelStr ;
existence
ex b₁ being RelStr st
( b₁ is trivial & b₁ is reflexive & b₁ is transitive & b₁ is antisymmetric & b₁ is with_suprema & b₁ is with_infima & b₁ is lower-bounded & not b₁ is empty & b₁ is finite & b₁ 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;