:: WAYBEL14 semantic presentation

theorem Th1: :: WAYBEL14:1

for b₁ being set
for b₂ being finite Subset-Family of b₁ ex b₃ being finite Subset-Family of b₁ st
( b₃ c= b₂ & union b₃ = union b₂ & ( for b₄ being Subset of b₁ st b₄ in b₃ holds
not b₄ c= union (b₃ \ {b₄}) ) )

proof end;

Lemma2: for b₁ being 1-sorted
for b₂, b₃ being Subset of b₁ holds
( b₂ c= b₃ ` iff b₃ c= b₂ ` )

proof end;

theorem Th2: :: WAYBEL14:2

for b₁ being 1-sorted
for b₂ being Subset of b₁ holds
( b₂ ` = the carrier of b₁ iff b₂ is empty )

proof end;

theorem Th3: :: WAYBEL14:3

for b₁ being non empty transitive antisymmetric with_infima RelStr
for b₂, b₃ being Element of b₁ holds downarrow (b₂ "/\" b₃) = (downarrow b₂) /\ (downarrow b₃)

proof end;

theorem Th4: :: WAYBEL14:4

for b₁ being non empty transitive antisymmetric with_suprema RelStr
for b₂, b₃ being Element of b₁ holds uparrow (b₂ "\/" b₃) = (uparrow b₂) /\ (uparrow b₃)

proof end;

theorem Th5: :: WAYBEL14:5

for b₁ being non empty antisymmetric complete RelStr
for b₂ being lower Subset of b₁ st sup b₂ in b₂ holds
b₂ = downarrow (sup b₂)

proof end;

theorem Th6: :: WAYBEL14:6

for b₁ being non empty antisymmetric complete RelStr
for b₂ being upper Subset of b₁ st inf b₂ in b₂ holds
b₂ = uparrow (inf b₂)

proof end;

theorem Th7: :: WAYBEL14:7

for b₁ being non empty reflexive transitive RelStr
for b₂, b₃ being Element of b₁ holds
( b₂ << b₃ iff uparrow b₃ c= wayabove b₂ )

proof end;

theorem Th8: :: WAYBEL14:8

for b₁ being non empty reflexive transitive RelStr
for b₂, b₃ being Element of b₁ holds
( b₂ << b₃ iff downarrow b₂ c= waybelow b₃ )

proof end;

theorem Th9: :: WAYBEL14:9

for b₁ being non empty reflexive antisymmetric complete RelStr
for b₂ being Element of b₁ holds
( sup (waybelow b₂) <= b₂ & b₂ <= inf (wayabove b₂) )

proof end;

theorem Th10: :: WAYBEL14:10

for b₁ being non empty antisymmetric lower-bounded RelStr holds uparrow (Bottom b₁) = the carrier of b₁

proof end;

theorem Th11: :: WAYBEL14:11

for b₁ being non empty antisymmetric upper-bounded RelStr holds downarrow (Top b₁) = the carrier of b₁

proof end;

theorem Th12: :: WAYBEL14:12

for b₁ being with_suprema Poset
for b₂, b₃ being Element of b₁ holds (wayabove b₂) "\/" (wayabove b₃) c= uparrow (b₂ "\/" b₃)

proof end;

theorem Th13: :: WAYBEL14:13

for b₁ being with_infima Poset
for b₂, b₃ being Element of b₁ holds (waybelow b₂) "/\" (waybelow b₃) c= downarrow (b₂ "/\" b₃)

proof end;

theorem Th14: :: WAYBEL14:14

for b₁ being non empty with_suprema Poset
for b₂ being Element of b₁ holds
( b₂ is co-prime iff for b₃, b₄ being Element of b₁ holds
( not b₂ <= b₃ "\/" b₄ or b₂ <= b₃ or b₂ <= b₄ ) )

proof end;

theorem Th15: :: WAYBEL14:15

for b₁ being non empty complete Poset
for b₂ being non empty Subset of b₁ holds downarrow (inf b₂) = meet { (downarrow b₃) where B is Element of b₁ : b₃ in b₂ }

proof end;

theorem Th16: :: WAYBEL14:16

for b₁ being non empty complete Poset
for b₂ being non empty Subset of b₁ holds uparrow (sup b₂) = meet { (uparrow b₃) where B is Element of b₁ : b₃ in b₂ }

proof end;

registration

let c₁ be sup-Semilattice;
let c₂ be Element of c₁;
cluster compactbelow a₂ -> directed ;
coherence

proof end;

end;

theorem Th17: :: WAYBEL14:17

for b₁ being non empty TopSpace
for b₂ being irreducible Subset of b₁
for b₃ being Element of (InclPoset the topology of b₁) st b₃ = b₂ ` holds
b₃ is prime

proof end;

theorem Th18: :: WAYBEL14:18

for b₁ being non empty TopSpace
for b₂, b₃ being Element of (InclPoset the topology of b₁) holds
( b₂ "\/" b₃ = b₂ \/ b₃ & b₂ "/\" b₃ = b₂ /\ b₃ )

proof end;

theorem Th19: :: WAYBEL14:19

for b₁ being non empty TopSpace
for b₂ being Element of (InclPoset the topology of b₁) holds
( b₂ is prime iff for b₃, b₄ being Element of (InclPoset the topology of b₁) holds
( not b₃ /\ b₄ c= b₂ or b₃ c= b₂ or b₄ c= b₂ ) )

proof end;

theorem Th20: :: WAYBEL14:20

for b₁ being non empty TopSpace
for b₂ being Element of (InclPoset the topology of b₁) holds
( b₂ is co-prime iff for b₃, b₄ being Element of (InclPoset the topology of b₁) holds
( not b₂ c= b₃ \/ b₄ or b₂ c= b₃ or b₂ c= b₄ ) )

proof end;

registration

let c₁ be non empty TopSpace;
cluster InclPoset the topology of a₁ -> distributive ;
coherence

proof end;

end;

theorem Th21: :: WAYBEL14:21

for b₁ being non empty TopSpace
for b₂ being TopLattice
for b₃ being Point of b₁
for b₄ being Point of b₂
for b₅ being Subset-Family of b₂ st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₃ = b₄ & b₅ is Basis of b₄ holds
b₅ is Basis of b₃

proof end;

theorem Th22: :: WAYBEL14:22

for b₁ being TopLattice
for b₂ being Element of b₁ st ( for b₃ being Subset of b₁ st b₃ is open holds
b₃ is upper ) holds
uparrow b₂ is compact

proof end;

registration

let c₁ be complete LATTICE;
cluster sigma a₁ -> non empty ;
coherence

proof end;

end;

theorem Th23: :: WAYBEL14:23

for b₁ being complete Scott TopLattice holds sigma b₁ = the topology of b₁

proof end;

theorem Th24: :: WAYBEL14:24

for b₁ being complete Scott TopLattice
for b₂ being Subset of b₁ holds
( b₂ in sigma b₁ iff b₂ is open )

proof end;

Lemma19: for b₁ being complete Scott TopLattice
for b₂ being filtered Subset of b₁
for b₃ being Subset-Family of b₁
for b₄ being Subset of (InclPoset (sigma b₁)) st b₃ = { (downarrow b₅) where B is Element of b₁ : b₅ in b₂ } & b₄ = COMPLEMENT b₃ holds
b₄ is directed

proof end;

theorem Th25: :: WAYBEL14:25

for b₁ being complete Scott TopLattice
for b₂ being Subset of (InclPoset (sigma b₁))
for b₃ being filtered Subset of b₁ st b₂ = { ((downarrow b₄) ` ) where B is Element of b₁ : b₄ in b₃ } holds
b₂ is directed

proof end;

theorem Th26: :: WAYBEL14:26

for b₁ being complete Scott TopLattice
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₃ is open & b₂ in b₃ holds
inf b₃ << b₂

proof end;

definition

let c₁ be non empty reflexive RelStr ;
let c₂ be Function of [:c₁,c₁:],c₁;
attr a₂ is jointly_Scott-continuous means :Def1: :: WAYBEL14:def 1
for b₁ being non empty TopSpace st TopStruct(# the carrier of b₁,the topology of b₁ #) = ConvergenceSpace (Scott-Convergence a₁) holds
ex b₂ being Function of [:b₁,b₁:],b₁ st
( b₂ = a₂ & b₂ is continuous );

end;

:: deftheorem Def1 defines jointly_Scott-continuous WAYBEL14:def 1 :

theorem Th27: :: WAYBEL14:27

for b₁ being complete Scott TopLattice
for b₂ being Subset of b₁
for b₃ being Element of (InclPoset (sigma b₁)) st b₃ = b₂ holds
( b₃ is co-prime iff ( b₂ is filtered & b₂ is upper ) )

proof end;

theorem Th28: :: WAYBEL14:28

for b₁ being complete Scott TopLattice
for b₂ being Subset of b₁
for b₃ being Element of (InclPoset (sigma b₁)) st b₃ = b₂ & ex b₄ being Element of b₁ st b₂ = (downarrow b₄) ` holds
( b₃ is prime & b₃ <> the carrier of b₁ )

proof end;

theorem Th29: :: WAYBEL14:29

for b₁ being complete Scott TopLattice
for b₂ being Subset of b₁
for b₃ being Element of (InclPoset (sigma b₁)) st b₃ = b₂ & sup_op b₁ is jointly_Scott-continuous & b₃ is prime & b₃ <> the carrier of b₁ holds
ex b₄ being Element of b₁ st b₂ = (downarrow b₄) `

proof end;

theorem Th30: :: WAYBEL14:30

for b₁ being complete Scott TopLattice st b₁ is continuous holds
sup_op b₁ is jointly_Scott-continuous

proof end;

theorem Th31: :: WAYBEL14:31

for b₁ being complete Scott TopLattice st sup_op b₁ is jointly_Scott-continuous holds
b₁ is sober

proof end;

theorem Th32: :: WAYBEL14:32

for b₁ being complete Scott TopLattice st b₁ is continuous holds
( b₁ is compact & b₁ is locally-compact & b₁ is sober & b₁ is Baire )

proof end;

theorem Th33: :: WAYBEL14:33

for b₁ being complete Scott TopLattice
for b₂ being Subset of b₁ st b₁ is continuous & b₂ in sigma b₁ holds
b₂ = union { (wayabove b₃) where B is Element of b₁ : b₃ in b₂ }

proof end;

theorem Th34: :: WAYBEL14:34

for b₁ being complete Scott TopLattice st ( for b₂ being Subset of b₁ st b₂ in sigma b₁ holds
b₂ = union { (wayabove b₃) where B is Element of b₁ : b₃ in b₂ } ) holds
b₁ is continuous

proof end;

theorem Th35: :: WAYBEL14:35

for b₁ being complete Scott TopLattice
for b₂ being Element of b₁ st b₁ is continuous holds
ex b₃ being Basis of b₂ st
for b₄ being Subset of b₁ st b₄ in b₃ holds
( b₄ is open & b₄ is filtered )

proof end;

theorem Th36: :: WAYBEL14:36

for b₁ being complete Scott TopLattice st b₁ is continuous holds
InclPoset (sigma b₁) is continuous

proof end;

theorem Th37: :: WAYBEL14:37

for b₁ being complete Scott TopLattice
for b₂ being Element of b₁ st ( for b₃ being Element of b₁ ex b₄ being Basis of b₃ st
for b₅ being Subset of b₁ st b₅ in b₄ holds
( b₅ is open & b₅ is filtered ) ) & InclPoset (sigma b₁) is continuous holds
b₂ = "\/" { (inf b₃) where B is Subset of b₁ : ( b₂ in b₃ & b₃ in sigma b₁ ) } ,b₁

proof end;

theorem Th38: :: WAYBEL14:38

for b₁ being complete Scott TopLattice st ( for b₂ being Element of b₁ holds b₂ = "\/" { (inf b₃) where B is Subset of b₁ : ( b₂ in b₃ & b₃ in sigma b₁ ) } ,b₁ ) holds
b₁ is continuous

proof end;

theorem Th39: :: WAYBEL14:39

for b₁ being complete Scott TopLattice holds
( ( for b₂ being Element of b₁ ex b₃ being Basis of b₂ st
for b₄ being Subset of b₁ st b₄ in b₃ holds
( b₄ is open & b₄ is filtered ) ) iff for b₂ being Element of (InclPoset (sigma b₁)) ex b₃ being Subset of (InclPoset (sigma b₁)) st
( b₂ = sup b₃ & ( for b₄ being Element of (InclPoset (sigma b₁)) st b₄ in b₃ holds
b₄ is co-prime ) ) )

proof end;

theorem Th40: :: WAYBEL14:40

for b₁ being complete Scott TopLattice holds
( ( ( for b₂ being Element of (InclPoset (sigma b₁)) ex b₃ being Subset of (InclPoset (sigma b₁)) st
( b₂ = sup b₃ & ( for b₄ being Element of (InclPoset (sigma b₁)) st b₄ in b₃ holds
b₄ is co-prime ) ) ) & InclPoset (sigma b₁) is continuous ) iff InclPoset (sigma b₁) is completely-distributive )

proof end;

theorem Th41: :: WAYBEL14:41

for b₁ being complete Scott TopLattice holds
( InclPoset (sigma b₁) is completely-distributive iff ( InclPoset (sigma b₁) is continuous & (InclPoset (sigma b₁)) opp is continuous ) )

proof end;

theorem Th42: :: WAYBEL14:42

for b₁ being complete Scott TopLattice st b₁ is algebraic holds
ex b₂ being Basis of b₁ st b₂ = { (uparrow b₃) where B is Element of b₁ : b₃ in the carrier of (CompactSublatt b₁) }

proof end;

theorem Th43: :: WAYBEL14:43

for b₁ being complete Scott TopLattice st ex b₂ being Basis of b₁ st b₂ = { (uparrow b₃) where B is Element of b₁ : b₃ in the carrier of (CompactSublatt b₁) } holds
( InclPoset (sigma b₁) is algebraic & ( for b₂ being Element of (InclPoset (sigma b₁)) ex b₃ being Subset of (InclPoset (sigma b₁)) st
( b₂ = sup b₃ & ( for b₄ being Element of (InclPoset (sigma b₁)) st b₄ in b₃ holds
b₄ is co-prime ) ) ) )

proof end;

theorem Th44: :: WAYBEL14:44

for b₁ being complete Scott TopLattice st InclPoset (sigma b₁) is algebraic & ( for b₂ being Element of (InclPoset (sigma b₁)) ex b₃ being Subset of (InclPoset (sigma b₁)) st
( b₂ = sup b₃ & ( for b₄ being Element of (InclPoset (sigma b₁)) st b₄ in b₃ holds
b₄ is co-prime ) ) ) holds
ex b₂ being Basis of b₁ st b₂ = { (uparrow b₃) where B is Element of b₁ : b₃ in the carrier of (CompactSublatt b₁) }

proof end;

theorem Th45: :: WAYBEL14:45

for b₁ being complete Scott TopLattice st ex b₂ being Basis of b₁ st b₂ = { (uparrow b₃) where B is Element of b₁ : b₃ in the carrier of (CompactSublatt b₁) } holds
b₁ is algebraic

proof end;