:: WAYBEL30 semantic presentation

theorem Th1: :: WAYBEL30:1

for b₁ being set
for b₂ being non empty set holds b₁ /\ (union b₂) = union { (b₁ /\ b₃) where B is Element of b₂ : verum }

proof end;

theorem Th2: :: WAYBEL30:2

for b₁ being non empty reflexive transitive RelStr
for b₂ being non empty directed Subset of (InclPoset (Ids b₁)) holds union b₂ is Ideal of b₁

proof end;

E3: now

let c₁ be non empty reflexive transitive RelStr ;
let c₂ be non empty directed Subset of (InclPoset (Ids c₁));
let c₃ be Element of (InclPoset (Ids c₁));
assume E4: c₃ = union c₂ ;
thus c₂ is_<=_than c₃

proof

let c₄ be Element of (InclPoset (Ids c₁)); :: according to LATTICE3:def 9
assume E5: c₄ in c₂ ;
c₄ c= c₃

proof

let c₅ be set ; :: according to TARSKI:def 3
assume c₅ in c₄ ;
hence c₅ in c₃ by E4, E5, TARSKI:def 4;

end;

hence c₄ <= c₃ by YELLOW_1:3;

end;

E4: now

let c₁ be non empty reflexive transitive RelStr ;
let c₂ be non empty directed Subset of (InclPoset (Ids c₁));
let c₃ be Element of (InclPoset (Ids c₁));
assume E5: c₃ = union c₂ ;
thus for b₁ being Element of (InclPoset (Ids c₁)) st b₁ is_>=_than c₂ holds
c₃ <= b₁

proof

let c₄ be Element of (InclPoset (Ids c₁));
assume E6: for b₁ being Element of (InclPoset (Ids c₁)) st b₁ in c₂ holds
c₄ >= b₁ ; :: according to LATTICE3:def 9
c₃ c= c₄

proof

let c₅ be set ; :: according to TARSKI:def 3
assume c₅ in c₃ ;
then consider c₆ being set such that
E7: ( c₅ in c₆ & c₆ in c₂ ) by E5, TARSKI:def 4;
reconsider c₇ = c₆ as Element of (InclPoset (Ids c₁)) by E7;
c₄ >= c₇ by E6, E7;
then c₇ c= c₄ by YELLOW_1:3;
hence c₅ in c₄ by E7;

end;

hence c₃ <= c₄ by YELLOW_1:3;

end;

registration

let c₁ be non empty reflexive transitive RelStr ;
cluster InclPoset (Ids a₁) -> up-complete ;
coherence

proof end;

end;

theorem Th3: :: WAYBEL30:3

for b₁ being non empty reflexive transitive RelStr
for b₂ being non empty directed Subset of (InclPoset (Ids b₁)) holds sup b₂ = union b₂

proof end;

theorem Th4: :: WAYBEL30:4

for b₁ being Semilattice
for b₂ being non empty directed Subset of (InclPoset (Ids b₁))
for b₃ being Element of (InclPoset (Ids b₁)) holds sup ({b₃} "/\" b₂) = union { (b₃ /\ b₄) where B is Element of b₂ : verum }

proof end;

registration

let c₁ be Semilattice;
cluster InclPoset (Ids a₁) -> up-complete satisfying_MC ;
coherence

proof end;

end;

registration

let c₁ be non empty trivial RelStr ;
cluster -> trivial TopAugmentation of a₁;
coherence

proof end;

end;

theorem Th5: :: WAYBEL30:5

for b₁ being complete Scott TopLattice
for b₂ being complete LATTICE
for b₃ being Scott TopAugmentation of b₂ st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
TopRelStr(# the carrier of b₃,the InternalRel of b₃,the topology of b₃ #) = TopRelStr(# the carrier of b₁,the InternalRel of b₁,the topology of b₁ #)

proof end;

theorem Th6: :: WAYBEL30:6

for b₁ being complete Lawson TopLattice
for b₂ being complete LATTICE
for b₃ being correct Lawson TopAugmentation of b₂ st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
TopRelStr(# the carrier of b₃,the InternalRel of b₃,the topology of b₃ #) = TopRelStr(# the carrier of b₁,the InternalRel of b₁,the topology of b₁ #)

proof end;

theorem Th7: :: WAYBEL30:7

for b₁ being complete Lawson TopLattice
for b₂ being Scott TopAugmentation of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ & b₄ is closed holds
b₃ is closed

proof end;

registration

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

proof end;

end;

registration

let c₁ be complete Scott TopLattice;
cluster InclPoset (sigma a₁) -> complete non trivial ;
coherence

proof end;

end;

registration

let c₁ be complete Lawson TopLattice;
cluster InclPoset (sigma a₁) -> complete non trivial ;
coherence

proof end;

cluster InclPoset (lambda a₁) -> complete non trivial ;
coherence

proof end;

end;

theorem Th8: :: WAYBEL30:8

for b₁ being non empty reflexive RelStr holds sigma b₁ c= { (b₂ \ (uparrow b₃)) where B is Subset of b₁, B is Subset of b₁ : ( b₂ in sigma b₁ & b₃ is finite ) }

proof end;

theorem Th9: :: WAYBEL30:9

for b₁ being complete Lawson TopLattice holds lambda b₁ = the topology of b₁

proof end;

theorem Th10: :: WAYBEL30:10

for b₁ being complete Lawson TopLattice holds sigma b₁ c= lambda b₁

proof end;

theorem Th11: :: WAYBEL30:11

for b₁, b₂ being complete LATTICE st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
lambda b₁ = lambda b₂

proof end;

theorem Th12: :: WAYBEL30:12

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

proof end;

registration

cluster non empty TopSpace-like reflexive trivial -> non empty reflexive Scott TopRelStr ;
coherence

proof end;

end;

registration

cluster complete trivial -> complete Lawson TopRelStr ;
coherence

proof end;

end;

registration

cluster complete lower-bounded meet-continuous strict Scott continuous TopRelStr ;
existence

proof end;

end;

registration

cluster complete compact Hausdorff strict Lawson continuous TopRelStr ;
existence

proof end;

end;

scheme :: WAYBEL30:sch 1
s1{ F₁() -> Scott TopLattice, F₂() -> set , F₃( set ) -> set } :

{ F₃(b₁) where B is Element of F₁() : b₁ in {} } = {}

proof end;

theorem Th13: :: WAYBEL30:13

for b₁ being meet-continuous LATTICE
for b₂ being Subset of b₁ st b₂ has_the_property_(S) holds
uparrow b₂ has_the_property_(S)

proof end;

registration

let c₁ be meet-continuous LATTICE;
let c₂ be property(S) Subset of c₁;
cluster uparrow a₂ -> property(S) ;
coherence by Th13;

end;

theorem Th14: :: WAYBEL30:14

for b₁ being complete meet-continuous Lawson TopLattice
for b₂ being Scott TopAugmentation of b₁
for b₃ being Subset of b₁ st b₃ in lambda b₁ holds
uparrow b₃ in sigma b₂

proof end;

theorem Th15: :: WAYBEL30:15

for b₁ being complete meet-continuous Lawson TopLattice
for b₂ being Scott TopAugmentation of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ & b₃ is open holds
uparrow b₄ is open

proof end;

theorem Th16: :: WAYBEL30:16

for b₁ being complete meet-continuous Lawson TopLattice
for b₂ being Scott TopAugmentation of b₁
for b₃ being Point of b₂
for b₄ being Point of b₁
for b₅ being Basis of b₄ st b₃ = b₄ holds
{ (uparrow b₆) where B is Subset of b₁ : b₆ in b₅ } is Basis of b₃

proof end;

theorem Th17: :: WAYBEL30:17

for b₁ being complete meet-continuous Lawson TopLattice
for b₂ being Scott TopAugmentation of b₁
for b₃ being upper Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
Int b₃ = Int b₄

proof end;

theorem Th18: :: WAYBEL30:18

for b₁ being complete meet-continuous Lawson TopLattice
for b₂ being Scott TopAugmentation of b₁
for b₃ being lower Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
Cl b₃ = Cl b₄

proof end;

theorem Th19: :: WAYBEL30:19

for b₁, b₂ being complete LATTICE
for b₃ being correct Lawson TopAugmentation of b₁
for b₄ being correct Lawson TopAugmentation of b₂ st InclPoset (sigma b₂) is continuous holds
the topology of [:b₃,b₄:] = lambda [:b₁,b₂:]

proof end;

theorem Th20: :: WAYBEL30:20

for b₁, b₂ being complete LATTICE
for b₃ being correct Lawson TopAugmentation of [:b₁,b₂:]
for b₄ being correct Lawson TopAugmentation of b₁
for b₅ being correct Lawson TopAugmentation of b₂ st InclPoset (sigma b₂) is continuous holds
TopStruct(# the carrier of b₃,the topology of b₃ #) = [:b₄,b₅:]

proof end;

theorem Th21: :: WAYBEL30:21

for b₁ being complete meet-continuous Lawson TopLattice
for b₂ being Element of b₁ holds b₂ "/\" is continuous

proof end;

registration

let c₁ be complete meet-continuous Lawson TopLattice;
let c₂ be Element of c₁;
cluster a₂ "/\" -> continuous ;
coherence by Th21;

end;

theorem Th22: :: WAYBEL30:22

for b₁ being complete meet-continuous Lawson TopLattice st InclPoset (sigma b₁) is continuous holds
b₁ is topological_semilattice

proof end;

E20: now

let c₁, c₂, c₃, c₄ be set ;
assume E21: ( c₃ in c₁ & c₄ in c₂ ) ;
E22: dom <:(pr2 c₁,c₂),(pr1 c₁,c₂):> = (dom (pr2 c₁,c₂)) /\ (dom (pr1 c₁,c₂)) by FUNCT_3:def 8
.= (dom (pr2 c₁,c₂)) /\ [:c₁,c₂:] by FUNCT_3:def 5
.= [:c₁,c₂:] /\ [:c₁,c₂:] by FUNCT_3:def 6
.= [:c₁,c₂:] ;
[c₃,c₄] in [:c₁,c₂:] by E21, ZFMISC_1:106;
hence <:(pr2 c₁,c₂),(pr1 c₁,c₂):> . [c₃,c₄] = [((pr2 c₁,c₂) . [c₃,c₄]),((pr1 c₁,c₂) . [c₃,c₄])] by E22, FUNCT_3:def 8
.= [c₄,((pr1 c₁,c₂) . [c₃,c₄])] by E21, FUNCT_3:def 6
.= [c₄,c₃] by E21, FUNCT_3:def 5 ;

end;

theorem Th23: :: WAYBEL30:23

for b₁ being complete meet-continuous Lawson TopLattice st InclPoset (sigma b₁) is continuous holds
( b₁ is being_T2 iff for b₂ being Subset of [:b₁,b₁:] st b₂ = the InternalRel of b₁ holds
b₂ is closed )

proof end;

definition

let c₁ be non empty reflexive RelStr ;
let c₂ be Subset of c₁;
func c₂ ^0 -> Subset of a₁ equals :: WAYBEL30:def 1
{ b₁ where B is Element of a₁ : for b₁ being non empty directed Subset of a₁ st b₁ <= sup b₂ holds
a₂ meets b₂ } ;
coherence

proof end;

end;

:: deftheorem Def1 defines ^0 WAYBEL30:def 1 :

registration

let c₁ be non empty reflexive antisymmetric RelStr ;
let c₂ be empty Subset of c₁;
cluster a₂ ^0 -> empty ;
coherence

proof end;

end;

theorem Th24: :: WAYBEL30:24

for b₁ being non empty reflexive RelStr
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
b₂ ^0 c= b₃ ^0

proof end;

theorem Th25: :: WAYBEL30:25

for b₁ being non empty reflexive RelStr
for b₂ being Element of b₁ holds (uparrow b₂) ^0 = wayabove b₂

proof end;

theorem Th26: :: WAYBEL30:26

for b₁ being Scott TopLattice
for b₂ being upper Subset of b₁ holds Int b₂ c= b₂ ^0

proof end;

theorem Th27: :: WAYBEL30:27

for b₁ being non empty reflexive RelStr
for b₂, b₃ being Subset of b₁ holds (b₂ ^0 ) \/ (b₃ ^0 ) c= (b₂ \/ b₃) ^0

proof end;

theorem Th28: :: WAYBEL30:28

for b₁ being meet-continuous LATTICE
for b₂, b₃ being upper Subset of b₁ holds (b₂ ^0 ) \/ (b₃ ^0 ) = (b₂ \/ b₃) ^0

proof end;

theorem Th29: :: WAYBEL30:29

for b₁ being meet-continuous Scott TopLattice
for b₂ being finite Subset of b₁ holds Int (uparrow b₂) c= union { (wayabove b₃) where B is Element of b₁ : b₃ in b₂ }

proof end;

theorem Th30: :: WAYBEL30:30

for b₁ being complete Lawson TopLattice holds
( b₁ is continuous iff ( b₁ is meet-continuous & b₁ is being_T2 ) )

proof end;

registration

cluster complete Lawson continuous -> complete Hausdorff TopRelStr ;
coherence by Th30;
cluster complete meet-continuous Hausdorff Lawson -> complete continuous TopRelStr ;
coherence by Th30;

end;

definition

let c₁ be non empty TopRelStr ;
attr a₁ is with_small_semilattices means :: WAYBEL30:def 2
for b₁ being Point of a₁ ex b₂ being basis of b₁ st
for b₃ being Subset of a₁ st b₃ in b₂ holds
subrelstr b₃ is meet-inheriting;
attr a₁ is with_compact_semilattices means :: WAYBEL30:def 3
for b₁ being Point of a₁ ex b₂ being basis of b₁ st
for b₃ being Subset of a₁ st b₃ in b₂ holds
( subrelstr b₃ is meet-inheriting & b₃ is compact );
attr a₁ is with_open_semilattices means :Def4: :: WAYBEL30:def 4
for b₁ being Point of a₁ ex b₂ being Basis of b₁ st
for b₃ being Subset of a₁ st b₃ in b₂ holds
subrelstr b₃ is meet-inheriting;

end;

:: deftheorem Def2 defines with_small_semilattices WAYBEL30:def 2 :

:: deftheorem Def3 defines with_compact_semilattices WAYBEL30:def 3 :

:: deftheorem Def4 defines with_open_semilattices WAYBEL30:def 4 :

registration

cluster non empty TopSpace-like with_open_semilattices -> non empty TopSpace-like with_small_semilattices TopRelStr ;
coherence

proof end;

cluster non empty TopSpace-like with_compact_semilattices -> non empty TopSpace-like with_small_semilattices TopRelStr ;
coherence

proof end;

cluster non empty anti-discrete -> non empty with_small_semilattices with_open_semilattices TopRelStr ;
coherence

proof end;

cluster non empty TopSpace-like reflexive trivial -> non empty with_compact_semilattices TopRelStr ;
coherence

proof end;

end;

registration

cluster Hausdorff strict lower Lawson Scott trivial with_small_semilattices with_compact_semilattices with_open_semilattices TopRelStr ;
existence

proof end;

end;

theorem Th31: :: WAYBEL30:31

for b₁ being with_infima topological_semilattice TopPoset
for b₂ being Subset of b₁ st subrelstr b₂ is meet-inheriting holds
subrelstr (Cl b₂) is meet-inheriting

proof end;

theorem Th32: :: WAYBEL30:32

for b₁ being complete meet-continuous Lawson TopLattice
for b₂ being Scott TopAugmentation of b₁ holds
( ( for b₃ being Point of b₂ ex b₄ being Basis of b₃ st
for b₅ being Subset of b₂ st b₅ in b₄ holds
b₅ is Filter of b₂ ) iff b₁ is with_open_semilattices )

proof end;

theorem Th33: :: WAYBEL30:33

for b₁ being complete Lawson TopLattice
for b₂ being Scott TopAugmentation of b₁
for b₃ being Element of b₁ holds { (inf b₄) where B is Subset of b₂ : ( b₃ in b₄ & b₄ in sigma b₂ ) } c= { (inf b₄) where B is Subset of b₁ : ( b₃ in b₄ & b₄ in lambda b₁ ) }

proof end;

theorem Th34: :: WAYBEL30:34

for b₁ being complete meet-continuous Lawson TopLattice
for b₂ being Scott TopAugmentation of b₁
for b₃ being Element of b₁ holds { (inf b₄) where B is Subset of b₂ : ( b₃ in b₄ & b₄ in sigma b₂ ) } = { (inf b₄) where B is Subset of b₁ : ( b₃ in b₄ & b₄ in lambda b₁ ) }

proof end;

theorem Th35: :: WAYBEL30:35

for b₁ being complete meet-continuous Lawson TopLattice holds
( b₁ is continuous iff ( b₁ is with_open_semilattices & InclPoset (sigma b₁) is continuous ) )

proof end;

registration

cluster complete Lawson continuous -> complete Lawson with_small_semilattices with_open_semilattices TopRelStr ;
coherence

proof end;

end;

registration

let c₁ be complete Lawson continuous TopLattice;
cluster InclPoset (sigma a₁) -> complete continuous non trivial ;
coherence by Th35;

end;

theorem Th36: :: WAYBEL30:36

for b₁ being complete Lawson continuous TopLattice holds
( b₁ is compact & b₁ is being_T2 & b₁ is topological_semilattice & b₁ is with_open_semilattices )

proof end;

theorem Th37: :: WAYBEL30:37

for b₁ being complete Hausdorff Lawson topological_semilattice with_open_semilattices TopLattice holds b₁ is with_compact_semilattices

proof end;

theorem Th38: :: WAYBEL30:38

for b₁ being complete meet-continuous Hausdorff Lawson TopLattice
for b₂ being Element of b₁ holds b₂ = "\/" { (inf b₃) where B is Subset of b₁ : ( b₂ in b₃ & b₃ in lambda b₁ ) } ,b₁

proof end;

theorem Th39: :: WAYBEL30:39

for b₁ being complete meet-continuous Lawson TopLattice holds
( b₁ is continuous iff for b₂ being Element of b₁ holds b₂ = "\/" { (inf b₃) where B is Subset of b₁ : ( b₂ in b₃ & b₃ in lambda b₁ ) } ,b₁ )

proof end;

theorem Th40: :: WAYBEL30:40

for b₁ being complete meet-continuous Lawson TopLattice holds
( b₁ is algebraic iff ( b₁ is with_open_semilattices & InclPoset (sigma b₁) is algebraic ) )

proof end;

registration

let c₁ be complete algebraic meet-continuous Lawson TopLattice;
cluster InclPoset (sigma a₁) -> complete algebraic continuous non trivial ;
coherence by Th40;

end;