:: WAYBEL19 semantic presentation

definition

let c₁ be non empty TopRelStr ;
attr a₁ is lower means :Def1: :: WAYBEL19:def 1
{ ((uparrow b₁) ` ) where B is Element of a₁ : verum } is prebasis of a₁;

end;

:: deftheorem Def1 defines lower WAYBEL19:def 1 :

E2: now

let c₁, c₂ be non empty RelStr ;
assume E3: RelStr(# the carrier of c₁,the InternalRel of c₁ #) = RelStr(# the carrier of c₂,the InternalRel of c₂ #) ;
set c₃ = { ((uparrow b₁) ` ) where B is Element of c₁ : verum } ;
set c₄ = { ((uparrow b₁) ` ) where B is Element of c₂ : verum } ;
thus { ((uparrow b₁) ` ) where B is Element of c₁ : verum } = { ((uparrow b₁) ` ) where B is Element of c₂ : verum }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10

let c₅ be set ;
assume c₅ in { ((uparrow b₁) ` ) where B is Element of c₁ : verum } ;
then consider c₆ being Element of c₁ such that
E4: c₅ = (uparrow c₆) ` ;
reconsider c₇ = c₆ as Element of c₂ by E3;
c₅ = ([#] c₁) \ (uparrow c₆) by E4, PRE_TOPC:17
.= ([#] c₁) \ (uparrow {c₆})
.= ([#] c₁) \ (uparrow {c₇}) by E3, WAYBEL_0:13
.= the carrier of c₁ \ (uparrow {c₇})
.= ([#] c₂) \ (uparrow {c₇}) by E3
.= (uparrow {c₇}) ` by PRE_TOPC:17
.= (uparrow c₇) ` ;
hence c₅ in { ((uparrow b₁) ` ) where B is Element of c₂ : verum } ;

end;

let c₅ be set ; :: according to TARSKI:def 3
assume c₅ in { ((uparrow b₁) ` ) where B is Element of c₂ : verum } ;
then consider c₆ being Element of c₂ such that
E4: c₅ = (uparrow c₆) ` ;
reconsider c₇ = c₆ as Element of c₁ by E3;
c₅ = ([#] c₂) \ (uparrow c₆) by E4, PRE_TOPC:17
.= ([#] c₂) \ (uparrow {c₆})
.= ([#] c₂) \ (uparrow {c₇}) by E3, WAYBEL_0:13
.= the carrier of c₁ \ (uparrow {c₇}) by E3
.= ([#] c₁) \ (uparrow {c₇})
.= (uparrow {c₇}) ` by PRE_TOPC:17
.= (uparrow c₇) ` ;
hence c₅ in { ((uparrow b₁) ` ) where B is Element of c₁ : verum } ;

end;

registration

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

proof end;

end;

registration

cluster strict complete trivial lower TopRelStr ;
existence

proof end;

end;

theorem Th1: :: WAYBEL19:1

for b₁ being non empty RelStr ex b₂ being correct strict TopAugmentation of b₁ st b₂ is lower

proof end;

registration

let c₁ be non empty RelStr ;
cluster correct strict lower TopAugmentation of a₁;
existence by Th1;

end;

theorem Th2: :: WAYBEL19:2

for b₁, b₂ being non empty TopSpace-like lower TopRelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
the topology of b₁ = the topology of b₂

proof end;

definition

let c₁ be non empty RelStr ;
func omega c₁ -> Subset-Family of a₁ means :Def2: :: WAYBEL19:def 2
for b₁ being correct lower TopAugmentation of a₁ holds a₂ = the topology of b₁;
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def2 defines omega WAYBEL19:def 2 :

theorem Th3: :: WAYBEL19:3

for b₁, b₂ being non empty RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
omega b₁ = omega b₂

proof end;

theorem Th4: :: WAYBEL19:4

for b₁ being non empty lower TopRelStr
for b₂ being Point of b₁ holds
( (uparrow b₂) ` is open & uparrow b₂ is closed )

proof end;

theorem Th5: :: WAYBEL19:5

for b₁ being non empty transitive lower TopRelStr
for b₂ being Subset of b₁ st b₂ is open holds
b₂ is lower

proof end;

theorem Th6: :: WAYBEL19:6

for b₁ being non empty transitive lower TopRelStr
for b₂ being Subset of b₁ st b₂ is closed holds
b₂ is upper

proof end;

theorem Th7: :: WAYBEL19:7

for b₁ being non empty TopSpace-like TopRelStr holds
( b₁ is lower iff { ((uparrow b₂) ` ) where B is Subset of b₁ : b₂ is finite } is Basis of b₁ )

proof end;

theorem Th8: :: WAYBEL19:8

for b₁, b₂ being complete lower TopLattice
for b₃ being Function of b₁,b₂ st ( for b₄ being non empty Subset of b₁ holds b₃ preserves_inf_of b₄ ) holds
b₃ is continuous

proof end;

theorem Th9: :: WAYBEL19:9

for b₁, b₂ being complete lower TopLattice
for b₃ being Function of b₁,b₂ st b₃ is infs-preserving holds
b₃ is continuous

proof end;

theorem Th10: :: WAYBEL19:10

for b₁ being complete lower TopLattice
for b₂ being prebasis of b₁
for b₃ being non empty filtered Subset of b₁ st ( for b₄ being Subset of b₁ st b₄ in b₂ & inf b₃ in b₄ holds
b₃ meets b₄ ) holds
inf b₃ in Cl b₃

proof end;

theorem Th11: :: WAYBEL19:11

for b₁, b₂ being complete lower TopLattice
for b₃ being Function of b₁,b₂ st b₃ is continuous holds
b₃ is filtered-infs-preserving

proof end;

theorem Th12: :: WAYBEL19:12

for b₁, b₂ being complete lower TopLattice
for b₃ being Function of b₁,b₂ st b₃ is continuous & ( for b₄ being finite Subset of b₁ holds b₃ preserves_inf_of b₄ ) holds
b₃ is infs-preserving

proof end;

theorem Th13: :: WAYBEL19:13

for b₁ being non empty reflexive transitive TopSpace-like lower TopRelStr
for b₂ being Point of b₁ holds Cl {b₂} = uparrow b₂

proof end;

definition

mode TopPoset is reflexive transitive antisymmetric TopSpace-like TopRelStr ;

end;

registration

cluster non empty lower -> non empty T_0 TopRelStr ;
coherence

proof end;

end;

registration

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

proof end;

end;

theorem Th14: :: WAYBEL19:14

for b₁, b₂ being non empty RelStr
for b₃ being Element of b₁
for b₄ being Element of b₂ holds (uparrow [b₃,b₄]) ` = [:((uparrow b₃) ` ),the carrier of b₂:] \/ [:the carrier of b₁,((uparrow b₄) ` ):]

proof end;

Lemma16: for b₁, b₂ being non empty RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) holds
for b₃ being Element of b₁
for b₄ being Element of b₂ st b₃ = b₄ holds
( uparrow b₃ = uparrow b₄ & downarrow b₃ = downarrow b₄ )
by WAYBEL_0:13;

theorem Th15: :: WAYBEL19:15

for b₁, b₂ being non empty lower-bounded Poset
for b₃ being correct lower TopAugmentation of b₁
for b₄ being correct lower TopAugmentation of b₂ holds omega [:b₁,b₂:] = the topology of [:b₃,b₄:]

proof end;

theorem Th16: :: WAYBEL19:16

for b₁, b₂ being non empty lower-bounded lower TopPoset holds omega [:b₁,b₂:] = the topology of [:b₁,b₂:]

proof end;

theorem Th17: :: WAYBEL19:17

for b₁, b₂ being complete lower TopLattice st b₂ is TopAugmentation of [:b₁,b₁:] holds
for b₃ being Function of b₂,b₁ st b₃ = inf_op b₁ holds
b₃ is continuous

proof end;

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

for b₁ being Subset of F₁() st b₁ is open holds
P₁[b₁]

provided

E18: ex b₁ being prebasis of F₁() st
for b₂ being Subset of F₁() st b₂ in b₁ holds
P₁[b₂] and
E19: for b₁ being Subset-Family of F₁() st ( for b₂ being Subset of F₁() st b₂ in b₁ holds
P₁[b₂] ) holds
P₁[ union b₁] and
E20: for b₁, b₂ being Subset of F₁() st P₁[b₁] & P₁[b₂] holds
P₁[b₁ /\ b₂] and
E21: P₁[ [#] F₁()]

proof end;

theorem Th18: :: WAYBEL19:18

for b₁, b₂ being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & ( for b₃ being Element of b₁ holds
( waybelow b₃ is directed & not waybelow b₃ is empty ) ) & b₁ is satisfying_axiom_of_approximation holds
b₂ is satisfying_axiom_of_approximation

proof end;

registration

let c₁ be non empty continuous Poset;
cluster -> continuous TopAugmentation of a₁;
coherence

proof end;

end;

theorem Th19: :: WAYBEL19:19

for b₁, b₂ being TopSpace
for b₃ being Refinement of b₁,b₂
for b₄ being Subset of b₃ st ( b₄ in the topology of b₁ or b₄ in the topology of b₂ ) holds
b₄ is open

proof end;

theorem Th20: :: WAYBEL19:20

for b₁, b₂ being TopSpace
for b₃ being Refinement of b₁,b₂
for b₄ being Subset of b₁
for b₅ being Subset of b₃ st b₅ = b₄ & b₄ is open holds
b₅ is open

proof end;

theorem Th21: :: WAYBEL19:21

for b₁, b₂ being TopSpace st the carrier of b₁ = the carrier of b₂ holds
for b₃ being Refinement of b₁,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;

theorem Th22: :: WAYBEL19:22

for b₁ being non empty TopSpace
for b₂, b₃ being set st b₂ c= b₃ & b₃ c= the topology of b₁ holds
( ( b₂ is Basis of b₁ implies b₃ is Basis of b₁ ) & ( b₂ is prebasis of b₁ implies b₃ is prebasis of b₁ ) )

proof end;

theorem Th23: :: WAYBEL19:23

for b₁, b₂ being non empty TopSpace st the carrier of b₁ = the carrier of b₂ holds
for b₃ being Refinement of b₁,b₂
for b₄ being prebasis of b₁
for b₅ being prebasis of b₂ holds b₄ \/ b₅ is prebasis of b₃

proof end;

theorem Th24: :: WAYBEL19:24

for b₁, b₂, b₃, b₄ being non empty TopSpace
for b₅ being Refinement of b₁,b₂
for b₆ being Refinement of b₃,b₄
for b₇ being Function of b₁,b₃
for b₈ being Function of b₂,b₄
for b₉ being Function of b₅,b₆ st b₉ = b₇ & b₉ = b₈ & b₇ is continuous & b₈ is continuous holds
b₉ is continuous

proof end;

theorem Th25: :: WAYBEL19:25

for b₁ being non empty TopSpace
for b₂ being prebasis of b₁
for b₃ being net of b₁
for b₄ being Point of b₁ st ( for b₅ being Subset of b₁ st b₄ in b₅ & b₅ in b₂ holds
b₃ is_eventually_in b₅ ) holds
b₄ in Lim b₃

proof end;

theorem Th26: :: WAYBEL19:26

for b₁ being non empty TopSpace
for b₂ being net of b₁
for b₃ being Subset of b₁ st b₂ is_eventually_in b₃ holds
Lim b₂ c= Cl b₃

proof end;

theorem Th27: :: WAYBEL19:27

for b₁ being non empty RelStr
for b₂ being non empty Subset of b₁ holds
( the mapping of (b₂ +id ) = id b₂ & the mapping of (b₂ opp+id ) = id b₂ )

proof end;

theorem Th28: :: WAYBEL19:28

for b₁ being non empty reflexive antisymmetric RelStr
for b₂ being Element of b₁ holds (uparrow b₂) /\ (downarrow b₂) = {b₂}

proof end;

definition

let c₁ be non empty reflexive TopRelStr ;
attr a₁ is Lawson means :Def3: :: WAYBEL19:def 3
(omega a₁) \/ (sigma a₁) is prebasis of a₁;

end;

:: deftheorem Def3 defines Lawson WAYBEL19:def 3 :

theorem Th29: :: WAYBEL19:29

for b₁ being complete LATTICE
for b₂ being correct lower TopAugmentation of b₁
for b₃ being Scott TopAugmentation of b₁
for b₄ being correct TopAugmentation of b₁ holds
( b₄ is Lawson iff b₄ is Refinement of b₃,b₂ )

proof end;

registration

let c₁ be complete LATTICE;
cluster lower-bounded correct strict Lawson TopAugmentation of a₁;
existence

proof end;

end;

registration

cluster strict Scott complete TopRelStr ;
existence

proof end;

cluster continuous strict complete Lawson TopRelStr ;
existence

proof end;

end;

theorem Th30: :: WAYBEL19:30

for b₁ being complete Lawson TopLattice holds (sigma b₁) \/ { ((uparrow b₂) ` ) where B is Element of b₁ : verum } is prebasis of b₁

proof end;

theorem Th31: :: WAYBEL19:31

for b₁ being complete Lawson TopLattice holds (sigma b₁) \/ { (b₂ \ (uparrow b₃)) where B is Subset of b₁, B is Element of b₁ : b₂ in sigma b₁ } is prebasis of b₁

proof end;

theorem Th32: :: WAYBEL19:32

for b₁ being complete Lawson TopLattice holds { (b₂ \ (uparrow b₃)) where B is Subset of b₁, B is Subset of b₁ : ( b₂ in sigma b₁ & b₃ is finite ) } is Basis of b₁

proof end;

definition

let c₁ be complete LATTICE;
func lambda c₁ -> Subset-Family of a₁ means :Def4: :: WAYBEL19:def 4
for b₁ being correct Lawson TopAugmentation of a₁ holds a₂ = the topology of b₁;
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def4 defines lambda WAYBEL19:def 4 :

theorem Th33: :: WAYBEL19:33

for b₁ being complete LATTICE holds lambda b₁ = UniCl (FinMeetCl ((sigma b₁) \/ (omega b₁)))

proof end;

theorem Th34: :: WAYBEL19:34

for b₁ being complete LATTICE
for b₂ being correct lower TopAugmentation of b₁
for b₃ being correct Scott TopAugmentation of b₁
for b₄ being Refinement of b₃,b₂ holds lambda b₁ = the topology of b₄

proof end;

Lemma32: for b₁ being LATTICE
for b₂ being Subset-Family of b₁ st ( for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ has_the_property_(S) ) holds
union b₂ has_the_property_(S)

proof end;

Lemma33: for b₁ being LATTICE
for b₂, b₃ being Subset of b₁ st b₂ has_the_property_(S) & b₃ has_the_property_(S) holds
b₂ /\ b₃ has_the_property_(S)

proof end;

Lemma34: for b₁ being LATTICE holds [#] b₁ has_the_property_(S)

proof end;

theorem Th35: :: WAYBEL19:35

for b₁ being up-complete lower TopLattice
for b₂ being Subset of b₁ st b₂ is open holds
b₂ has_the_property_(S)

proof end;

theorem Th36: :: WAYBEL19:36

for b₁ being complete Lawson TopLattice
for b₂ being Subset of b₁ st b₂ is open holds
b₂ has_the_property_(S)

proof end;

theorem Th37: :: WAYBEL19:37

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

proof end;

theorem Th38: :: WAYBEL19:38

for b₁ being complete Lawson TopLattice
for b₂ being Element of b₁ holds
( uparrow b₂ is closed & downarrow b₂ is closed & {b₂} is closed )

proof end;

theorem Th39: :: WAYBEL19:39

for b₁ being complete Lawson TopLattice
for b₂ being Element of b₁ holds
( (uparrow b₂) ` is open & (downarrow b₂) ` is open & {b₂} ` is open )

proof end;

theorem Th40: :: WAYBEL19:40

for b₁ being continuous complete Lawson TopLattice
for b₂ being Element of b₁ holds
( wayabove b₂ is open & (wayabove b₂) ` is closed )

proof end;

theorem Th41: :: WAYBEL19:41

for b₁ being Scott complete TopLattice
for b₂ being correct Lawson TopAugmentation of b₁
for b₃ being upper Subset of b₂ st b₃ is open holds
for b₄ being Subset of b₁ st b₄ = b₃ holds
b₄ is open

proof end;

theorem Th42: :: WAYBEL19:42

for b₁ being complete Lawson TopLattice
for b₂ being lower Subset of b₁ holds
( b₂ is closed iff b₂ is closed_under_directed_sups )

proof end;

theorem Th43: :: WAYBEL19:43

for b₁ being complete Lawson TopLattice
for b₂ being non empty filtered Subset of b₁ holds Lim (b₂ opp+id ) = {(inf b₂)}

proof end;

registration

cluster complete Lawson -> compact being_T1 complete TopRelStr ;
coherence

proof end;

end;

registration

cluster continuous complete Lawson -> continuous Hausdorff complete TopRelStr ;
coherence

proof end;

end;