:: WAYBEL19 semantic presentation

definition

let T be non empty TopRelStr ;
attr T is lower means :Def1: :: WAYBEL19:def 1
{ ((uparrow x) ` ) where x is Element of T : verum } is prebasis of T;

end;

:: deftheorem Def1 defines lower WAYBEL19:def 1 :

Lm1: now

let LL, T be non empty RelStr ; :: thesis:
assume A1: RelStr(# the carrier of LL,the InternalRel of LL #) = RelStr(# the carrier of T,the InternalRel of T #) ; :: thesis:
set A = { ((uparrow x) ` ) where x is Element of LL : verum } ;
set BB = { ((uparrow x) ` ) where x is Element of T : verum } ;
thus { ((uparrow x) ` ) where x is Element of LL : verum } = { ((uparrow x) ` ) where x is Element of T : verum } :: thesis:

proof

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

let a be set ; :: thesis:
assume a in { ((uparrow x) ` ) where x is Element of LL : verum } ; :: thesis:
then consider x being Element of LL such that
A2: a = (uparrow x) ` ;
reconsider y = x as Element of T by A1;
a = ([#] LL) \ (uparrow x) by A2, PRE_TOPC:17
.= ([#] LL) \ (uparrow {x})
.= ([#] LL) \ (uparrow {y}) by A1, WAYBEL_0:13
.= the carrier of LL \ (uparrow {y})
.= ([#] T) \ (uparrow {y}) by A1
.= (uparrow {y}) ` by PRE_TOPC:17
.= (uparrow y) ` ;
hence a in { ((uparrow x) ` ) where x is Element of T : verum } ; :: thesis:

end;

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in { ((uparrow x) ` ) where x is Element of T : verum } ; :: thesis:
then consider x being Element of T such that
A3: a = (uparrow x) ` ;
reconsider y = x as Element of LL by A1;
a = ([#] T) \ (uparrow x) by A3, PRE_TOPC:17
.= ([#] T) \ (uparrow {x})
.= ([#] T) \ (uparrow {y}) by A1, WAYBEL_0:13
.= the carrier of LL \ (uparrow {y}) by A1
.= ([#] LL) \ (uparrow {y})
.= (uparrow {y}) ` by PRE_TOPC:17
.= (uparrow y) ` ;
hence a in { ((uparrow x) ` ) where x is Element of LL : verum } ; :: thesis:

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 LL being non empty RelStr ex T being correct strict TopAugmentation of LL st T is lower

proof end;

registration

let R be non empty RelStr ;
cluster correct strict lower TopAugmentation of R;
existence by Th1;

end;

theorem Th2: :: WAYBEL19:2

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

proof end;

definition

let R be non empty RelStr ;
func omega R -> Subset-Family of R means :Def2: :: WAYBEL19:def 2
for T being correct lower TopAugmentation of R holds it = the topology of T;
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def2 defines omega WAYBEL19:def 2 :

theorem Th3: :: WAYBEL19:3

for R1, R2 being non empty RelStr st RelStr(# the carrier of R1,the InternalRel of R1 #) = RelStr(# the carrier of R2,the InternalRel of R2 #) holds
omega R1 = omega R2

proof end;

theorem Th4: :: WAYBEL19:4

for T being non empty lower TopRelStr
for x being Point of T holds
( (uparrow x) ` is open & uparrow x is closed )

proof end;

theorem Th5: :: WAYBEL19:5

for T being non empty transitive lower TopRelStr
for A being Subset of T st A is open holds
A is lower

proof end;

theorem Th6: :: WAYBEL19:6

for T being non empty transitive lower TopRelStr
for A being Subset of T st A is closed holds
A is upper

proof end;

theorem Th7: :: WAYBEL19:7

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

proof end;

theorem Th8: :: WAYBEL19:8

for S, T being complete lower TopLattice
for f being Function of S,T st ( for X being non empty Subset of S holds f preserves_inf_of X ) holds
f is continuous

proof end;

theorem Th9: :: WAYBEL19:9

for S, T being complete lower TopLattice
for f being Function of S,T st f is infs-preserving holds
f is continuous

proof end;

theorem Th10: :: WAYBEL19:10

for T being complete lower TopLattice
for BB being prebasis of T
for F being non empty filtered Subset of T st ( for A being Subset of T st A in BB & inf F in A holds
F meets A ) holds
inf F in Cl F

proof end;

theorem Th11: :: WAYBEL19:11

for S, T being complete lower TopLattice
for f being Function of S,T st f is continuous holds
f is filtered-infs-preserving

proof end;

theorem :: WAYBEL19:12

for S, T being complete lower TopLattice
for f being Function of S,T st f is continuous & ( for X being finite Subset of S holds f preserves_inf_of X ) holds
f is infs-preserving

proof end;

theorem :: WAYBEL19:13

for T being non empty reflexive transitive TopSpace-like lower TopRelStr
for x being Point of T holds Cl {x} = uparrow x

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 R be non empty lower-bounded RelStr ;
cluster -> lower-bounded TopAugmentation of R;
coherence

proof end;

end;

theorem Th14: :: WAYBEL19:14

for S, T being non empty RelStr
for s being Element of S
for t being Element of T holds (uparrow [s,t]) ` = [:((uparrow s) ` ),the carrier of T:] \/ [:the carrier of S,((uparrow t) ` ):]

proof end;

Lm2: for L1, L2 being non empty RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) holds
for x1 being Element of L1
for x2 being Element of L2 st x1 = x2 holds
( uparrow x1 = uparrow x2 & downarrow x1 = downarrow x2 )
by WAYBEL_0:13;

theorem Th15: :: WAYBEL19:15

for S, T being non empty lower-bounded Poset
for S' being correct lower TopAugmentation of S
for T' being correct lower TopAugmentation of T holds omega [:S,T:] = the topology of [:S',T':]

proof end;

theorem :: WAYBEL19:16

for S, T being non empty lower-bounded lower TopPoset holds omega [:S,T:] = the topology of [:S,T:]

proof end;

theorem :: WAYBEL19:17

for T, T2 being complete lower TopLattice st T2 is TopAugmentation of [:T,T:] holds
for f being Function of T2,T st f = inf_op T holds
f is continuous

proof end;

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

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

provided

A1: ex K being prebasis of F₁() st
for A being Subset of F₁() st A in K holds
P₁[A] and
A2: for F being Subset-Family of F₁() st ( for A being Subset of F₁() st A in F holds
P₁[A] ) holds
P₁[ union F] and
A3: for A1, A2 being Subset of F₁() st P₁[A1] & P₁[A2] holds
P₁[A1 /\ A2] and
A4: P₁[ [#] F₁()]

proof end;

theorem :: WAYBEL19:18

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

proof end;

registration

let T be non empty continuous Poset;
cluster -> continuous TopAugmentation of T;
coherence

proof end;

end;

theorem Th19: :: WAYBEL19:19

for T, S being TopSpace
for R being Refinement of T,S
for W being Subset of R st ( W in the topology of T or W in the topology of S ) holds
W is open

proof end;

theorem Th20: :: WAYBEL19:20

for T, S being TopSpace
for R being Refinement of T,S
for V being Subset of T
for W being Subset of R st W = V & V is open holds
W is open

proof end;

theorem Th21: :: WAYBEL19:21

for T, S being TopSpace st the carrier of T = the carrier of S holds
for R being Refinement of T,S
for V being Subset of T
for W being Subset of R st W = V & V is closed holds
W is closed

proof end;

theorem Th22: :: WAYBEL19:22

for T being non empty TopSpace
for K, O being set st K c= O & O c= the topology of T holds
( ( K is Basis of T implies O is Basis of T ) & ( K is prebasis of T implies O is prebasis of T ) )

proof end;

theorem Th23: :: WAYBEL19:23

for T1, T2 being non empty TopSpace st the carrier of T1 = the carrier of T2 holds
for T being Refinement of T1,T2
for B1 being prebasis of T1
for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T

proof end;

theorem :: WAYBEL19:24

for T1, S1, T2, S2 being non empty TopSpace
for R1 being Refinement of T1,S1
for R2 being Refinement of T2,S2
for f being Function of T1,T2
for g being Function of S1,S2
for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds
h is continuous

proof end;

theorem Th25: :: WAYBEL19:25

for T being non empty TopSpace
for K being prebasis of T
for N being net of T
for p being Point of T st ( for A being Subset of T st p in A & A in K holds
N is_eventually_in A ) holds
p in Lim N

proof end;

theorem Th26: :: WAYBEL19:26

for T being non empty TopSpace
for N being net of T
for S being Subset of T st N is_eventually_in S holds
Lim N c= Cl S

proof end;

theorem Th27: :: WAYBEL19:27

for R being non empty RelStr
for X being non empty Subset of R holds
( the mapping of (X +id ) = id X & the mapping of (X opp+id ) = id X )

proof end;

theorem Th28: :: WAYBEL19:28

for R being non empty reflexive antisymmetric RelStr
for x being Element of R holds (uparrow x) /\ (downarrow x) = {x}

proof end;

definition

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

end;

:: deftheorem Def3 defines Lawson WAYBEL19:def 3 :

theorem Th29: :: WAYBEL19:29

for R being complete LATTICE
for LL being correct lower TopAugmentation of R
for S being Scott TopAugmentation of R
for T being correct TopAugmentation of R holds
( T is Lawson iff T is Refinement of S,LL )

proof end;

registration

let R be complete LATTICE;
cluster lower-bounded correct strict Lawson TopAugmentation of R;
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 T being complete Lawson TopLattice holds (sigma T) \/ { ((uparrow x) ` ) where x is Element of T : verum } is prebasis of T

proof end;

theorem :: WAYBEL19:31

for T being complete Lawson TopLattice holds (sigma T) \/ { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } is prebasis of T

proof end;

theorem :: WAYBEL19:32

for T being complete Lawson TopLattice holds { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } is Basis of T

proof end;

definition

let T be complete LATTICE;
func lambda T -> Subset-Family of T means :Def4: :: WAYBEL19:def 4
for S being correct Lawson TopAugmentation of T holds it = the topology of S;
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def4 defines lambda WAYBEL19:def 4 :

theorem Th33: :: WAYBEL19:33

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

proof end;

theorem :: WAYBEL19:34

for R being complete LATTICE
for T being correct lower TopAugmentation of R
for S being correct Scott TopAugmentation of R
for M being Refinement of S,T holds lambda R = the topology of M

proof end;

Lm3: for T being LATTICE
for F being Subset-Family of T st ( for A being Subset of T st A in F holds
A has_the_property_(S) ) holds
union F has_the_property_(S)

proof end;

Lm4: for T being LATTICE
for A1, A2 being Subset of T st A1 has_the_property_(S) & A2 has_the_property_(S) holds
A1 /\ A2 has_the_property_(S)

proof end;

Lm5: for T being LATTICE holds [#] T has_the_property_(S)

proof end;

theorem Th35: :: WAYBEL19:35

for T being up-complete lower TopLattice
for A being Subset of T st A is open holds
A has_the_property_(S)

proof end;

theorem Th36: :: WAYBEL19:36

for T being complete Lawson TopLattice
for A being Subset of T st A is open holds
A has_the_property_(S)

proof end;

theorem Th37: :: WAYBEL19:37

for S being Scott complete TopLattice
for T being correct Lawson TopAugmentation of S
for A being Subset of S st A is open holds
for C being Subset of T st C = A holds
C is open

proof end;

theorem Th38: :: WAYBEL19:38

for T being complete Lawson TopLattice
for x being Element of T holds
( uparrow x is closed & downarrow x is closed & {x} is closed )

proof end;

theorem Th39: :: WAYBEL19:39

for T being complete Lawson TopLattice
for x being Element of T holds
( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open )

proof end;

theorem Th40: :: WAYBEL19:40

for T being continuous complete Lawson TopLattice
for x being Element of T holds
( wayabove x is open & (wayabove x) ` is closed )

proof end;

theorem :: WAYBEL19:41

for S being Scott complete TopLattice
for T being correct Lawson TopAugmentation of S
for A being upper Subset of T st A is open holds
for C being Subset of S st C = A holds
C is open

proof end;

theorem :: WAYBEL19:42

for T being complete Lawson TopLattice
for A being lower Subset of T holds
( A is closed iff A is closed_under_directed_sups )

proof end;

theorem :: WAYBEL19:43

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

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;