:: WAYBEL31 semantic presentation

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

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

proof end;

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

for b₁ being Subset-Family of F₁() st b₁ = { b₂ where B is Subset of F₁() : P₁[b₂] } holds
downarrow (union b₁) = union { (downarrow b₂) where B is Subset of F₁() : P₁[b₂] }

proof end;

registration

let c₁ be lower-bounded continuous sup-Semilattice;
let c₂ be with_bottom CLbasis of c₁;
cluster InclPoset (Ids (subrelstr a₂)) -> algebraic ;
coherence by WAYBEL13:10;

end;

definition

let c₁ be continuous sup-Semilattice;
func CLweight c₁ -> Cardinal equals :: WAYBEL31:def 1
meet { (Card b₁) where B is with_bottom CLbasis of a₁ : verum } ;
coherence

proof end;

end;

:: deftheorem Def1 defines CLweight WAYBEL31:def 1 :

theorem Th1: :: WAYBEL31:1

for b₁ being TopStruct
for b₂ being Basis of b₁ holds weight b₁ c= Card b₂

proof end;

theorem Th2: :: WAYBEL31:2

for b₁ being TopStruct ex b₂ being Basis of b₁ st Card b₂ = weight b₁

proof end;

theorem Th3: :: WAYBEL31:3

for b₁ being continuous sup-Semilattice
for b₂ being with_bottom CLbasis of b₁ holds CLweight b₁ c= Card b₂

proof end;

theorem Th4: :: WAYBEL31:4

for b₁ being continuous sup-Semilattice ex b₂ being with_bottom CLbasis of b₁ st Card b₂ = CLweight b₁

proof end;

theorem Th5: :: WAYBEL31:5

for b₁ being lower-bounded algebraic LATTICE holds CLweight b₁ = Card the carrier of (CompactSublatt b₁)

proof end;

theorem Th6: :: WAYBEL31:6

for b₁ being non empty TopSpace
for b₂ being continuous sup-Semilattice st InclPoset the topology of b₁ = b₂ holds
for b₃ being with_bottom CLbasis of b₂ holds b₃ is Basis of b₁

proof end;

theorem Th7: :: WAYBEL31:7

for b₁ being non empty TopSpace
for b₂ being lower-bounded continuous LATTICE st InclPoset the topology of b₁ = b₂ holds
for b₃ being Basis of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
finsups b₄ is with_bottom CLbasis of b₂

proof end;

theorem Th8: :: WAYBEL31:8

for b₁ being non empty T_0 TopSpace
for b₂ being lower-bounded continuous sup-Semilattice st InclPoset the topology of b₁ = b₂ & not b₁ is finite holds
weight b₁ = CLweight b₂

proof end;

theorem Th9: :: WAYBEL31:9

for b₁ being non empty T_0 TopSpace
for b₂ being continuous sup-Semilattice st InclPoset the topology of b₁ = b₂ holds
Card the carrier of b₁ c= Card the carrier of b₂

proof end;

theorem Th10: :: WAYBEL31:10

for b₁ being non empty T_0 TopSpace st b₁ is finite holds
weight b₁ = Card the carrier of b₁

proof end;

theorem Th11: :: WAYBEL31:11

for b₁ being TopStruct
for b₂ being lower-bounded continuous LATTICE st InclPoset the topology of b₁ = b₂ & b₁ is finite holds
CLweight b₂ = Card the carrier of b₂

proof end;

theorem Th12: :: WAYBEL31:12

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being Scott TopAugmentation of b₁
for b₃ being correct Lawson TopAugmentation of b₁
for b₄ being Basis of b₃ holds { (uparrow b₅) where B is Subset of b₃ : b₅ in b₄ } is Basis of b₂

proof end;

Lemma13: for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being Scott TopAugmentation of b₁
for b₃ being correct Lawson TopAugmentation of b₁ holds weight b₂ c= weight b₃

proof end;

theorem Th13: :: WAYBEL31:13

canceled;

theorem Th14: :: WAYBEL31:14

for b₁ being non empty up-complete Poset st b₁ is finite holds
for b₂ being Element of b₁ holds b₂ in compactbelow b₂

proof end;

theorem Th15: :: WAYBEL31:15

for b₁ being finite LATTICE holds b₁ is arithmetic

proof end;

registration

cluster finite -> arithmetic RelStr ;
coherence by Th15;

end;

registration

cluster non empty finite strict reflexive transitive antisymmetric lower-bounded arithmetic with_suprema with_infima trivial RelStr ;
existence

proof end;

end;

theorem Th16: :: WAYBEL31:16

for b₁ being finite LATTICE
for b₂ being with_bottom CLbasis of b₁ holds
( Card b₂ = CLweight b₁ iff b₂ = the carrier of (CompactSublatt b₁) )

proof end;

definition

let c₁ be non empty reflexive RelStr ;
let c₂ be Subset of c₁;
let c₃ be Element of c₁;
func Way_Up c₃,c₂ -> Subset of a₁ equals :: WAYBEL31:def 2
(wayabove a₃) \ (uparrow a₂);
coherence ;

end;

:: deftheorem Def2 defines Way_Up WAYBEL31:def 2 :

theorem Th17: :: WAYBEL31:17

for b₁ being non empty reflexive RelStr
for b₂ being Element of b₁ holds Way_Up b₂,({} b₁) = wayabove b₂ ;

theorem Th18: :: WAYBEL31:18

for b₁ being non empty Poset
for b₂ being Subset of b₁
for b₃ being Element of b₁ st b₃ in uparrow b₂ holds
Way_Up b₃,b₂ = {}

proof end;

theorem Th19: :: WAYBEL31:19

for b₁ being non empty finite reflexive transitive RelStr holds Ids b₁ is finite

proof end;

theorem Th20: :: WAYBEL31:20

for b₁ being lower-bounded continuous sup-Semilattice st not b₁ is finite holds
for b₂ being with_bottom CLbasis of b₁ holds not b₂ is finite

proof end;

theorem Th21: :: WAYBEL31:21

canceled;

theorem Th22: :: WAYBEL31:22

canceled;

theorem Th23: :: WAYBEL31:23

for b₁ being non empty complete Poset
for b₂ being Element of b₁ st b₂ is compact holds
b₂ = inf (wayabove b₂)

proof end;

theorem Th24: :: WAYBEL31:24

for b₁ being lower-bounded continuous sup-Semilattice st not b₁ is finite holds
for b₂ being with_bottom CLbasis of b₁ holds Card { (Way_Up b₃,b₄) where B is Element of b₁, B is finite Subset of b₁ : ( b₃ in b₂ & b₄ c= b₂ ) } c= Card b₂

proof end;

theorem Th25: :: WAYBEL31:25

for b₁ being complete Lawson TopLattice
for b₂ being finite Subset of b₁ holds
( (uparrow b₂) ` is open & (downarrow b₂) ` is open )

proof end;

theorem Th26: :: WAYBEL31:26

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being correct Lawson TopAugmentation of b₁
for b₃ being with_bottom CLbasis of b₁ holds { (Way_Up b₄,b₅) where B is Element of b₁, B is finite Subset of b₁ : ( b₄ in b₃ & b₅ c= b₃ ) } is Basis of b₂

proof end;

Lemma22: for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being correct Lawson TopAugmentation of b₁ holds weight b₂ c= CLweight b₁

proof end;

theorem Th27: :: WAYBEL31:27

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being Scott TopAugmentation of b₁
for b₃ being Basis of b₂ holds { (wayabove (inf b₄)) where B is Subset of b₂ : b₄ in b₃ } is Basis of b₂

proof end;

theorem Th28: :: WAYBEL31:28

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being Scott TopAugmentation of b₁
for b₃ being Basis of b₂ st not b₃ is finite holds
not { (inf b₄) where B is Subset of b₂ : b₄ in b₃ } is finite

proof end;

Lemma25: for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being Scott TopAugmentation of b₁ holds CLweight b₁ c= weight b₂

proof end;

theorem Th29: :: WAYBEL31:29

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being Scott TopAugmentation of b₁ holds CLweight b₁ = weight b₂

proof end;

theorem Th30: :: WAYBEL31:30

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being correct Lawson TopAugmentation of b₁ holds CLweight b₁ = weight b₂

proof end;

theorem Th31: :: WAYBEL31:31

for b₁, b₂ being non empty RelStr st b₁,b₂ are_isomorphic holds
Card the carrier of b₁ = Card the carrier of b₂

proof end;

theorem Th32: :: WAYBEL31:32

for b₁ being lower-bounded continuous sup-Semilattice
for b₂ being with_bottom CLbasis of b₁ st Card b₂ = CLweight b₁ holds
CLweight b₁ = CLweight (InclPoset (Ids (subrelstr b₂)))

proof end;

registration

let c₁ be lower-bounded continuous sup-Semilattice;
cluster InclPoset (sigma a₁) -> with_suprema continuous ;
coherence

proof end;

end;

theorem Th33: :: WAYBEL31:33

for b₁ being lower-bounded continuous sup-Semilattice holds CLweight b₁ c= CLweight (InclPoset (sigma b₁))

proof end;

theorem Th34: :: WAYBEL31:34

for b₁ being lower-bounded continuous sup-Semilattice st not b₁ is finite holds
CLweight b₁ = CLweight (InclPoset (sigma b₁))

proof end;