:: The Lawson Topology
:: by Grzegorz Bancerek
::
:: Received June 21, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users

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 :
for T being non empty TopRelStr holds
( T is lower iff { ((uparrow x) `) where x is Element of T : verum } is prebasis of T );

Lm1: now :: thesis: for LL, T being non empty RelStr st RelStr(# the carrier of LL, the InternalRel of LL #) = RelStr(# the carrier of T, the InternalRel of T #) holds
{ ((uparrow x) `) where x is Element of LL : verum } = { ((uparrow x) `) where x is Element of T : verum }

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

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { ((uparrow x) `) where x is Element of T : verum } c= { ((uparrow x) `) where x is Element of LL : verum }

let a be object ; :: thesis: ( a in { ((uparrow x) `) where x is Element of LL : verum } implies a in { ((uparrow x) `) where x is Element of T : verum } )
assume a in { ((uparrow x) `) where x is Element of LL : verum } ; :: thesis: a in { ((uparrow x) `) where x is Element of T : verum }
then consider x being Element of LL such that
A2: a = (uparrow x) ` ;
reconsider y = x as Element of T by A1;
a = (uparrow y) ` by A1, A2, WAYBEL_0:13;
hence a in { ((uparrow x) `) where x is Element of T : verum } ; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((uparrow x) `) where x is Element of T : verum } or a in { ((uparrow x) `) where x is Element of LL : verum } )
assume a in { ((uparrow x) `) where x is Element of T : verum } ; :: thesis: a in { ((uparrow x) `) where x is Element of LL : verum }
then consider x being Element of T such that
A3: a = (uparrow x) ` ;
reconsider y = x as Element of LL by A1;
a = (uparrow y) ` by A1, A3, WAYBEL_0:13;
hence a in { ((uparrow x) `) where x is Element of LL : verum } ; :: thesis: verum

end;

end;

registration

cluster 1 -element TopSpace-like reflexive -> 1 -element TopSpace-like reflexive lower for TopRelStr ;

coherence
for b₁ being 1 -element TopSpace-like reflexive TopRelStr holds b₁ is lower

proof end;

end;

registration

cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict non void lower for TopRelStr ;

existence
ex b₁ being TopLattice st
( b₁ is lower & b₁ is trivial & b₁ is complete & b₁ is strict )

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 non empty correct strict lower for TopAugmentation of R;

existence
ex b₁ being correct strict TopAugmentation of R st b₁ is lower 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
for b₁, b₂ being Subset-Family of R st ( for T being correct lower TopAugmentation of R holds b₁ = the topology of T ) & ( for T being correct lower TopAugmentation of R holds b₂ = the topology of T ) holds
b₁ = b₂

proof end;

existence
ex b₁ being Subset-Family of R st
for T being correct lower TopAugmentation of R holds b₁ = the topology of T

proof end;

end;

:: deftheorem Def2 defines omega WAYBEL19:def 2 :
for R being non empty RelStr
for b₂ being Subset-Family of R holds
( b₂ = omega R iff for T being correct lower TopAugmentation of R holds b₂ = the topology of T );

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 TopSpace-like reflexive transitive lower TopRelStr
for x being Point of T holds Cl {x} = uparrow x

proof end;

definition

mode TopPoset is TopSpace-like reflexive transitive antisymmetric TopRelStr ;

end;

registration

cluster non empty TopSpace-like reflexive transitive antisymmetric lower -> non empty T_0 for TopRelStr ;

coherence
for b₁ being non empty TopPoset st b₁ is lower holds
b₁ is T_0

proof end;

end;

registration

let R be non empty lower-bounded RelStr ;

cluster -> lower-bounded for TopAugmentation of R;

coherence
for b₁ being TopAugmentation of R holds b₁ is lower-bounded

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;

theorem Th15: :: WAYBEL19:15

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

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 for TopAugmentation of T;

coherence
for b₁ being TopAugmentation of T holds b₁ is continuous

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 by Th19;

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 :
for T being non empty reflexive TopRelStr holds
( T is Lawson iff (omega T) \/ (sigma T) is prebasis of T );

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 non empty correct reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V199() up-complete /\-complete strict non void Lawson for TopAugmentation of R;

existence
ex b₁ being TopAugmentation of R st
( b₁ is Lawson & b₁ is strict & b₁ is correct )

proof end;

end;

registration

cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict Scott non void for TopRelStr ;

existence
ex b₁ being TopLattice st
( b₁ is Scott & b₁ is complete & b₁ is strict )

proof end;

cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V199() continuous up-complete /\-complete strict non void Lawson for TopRelStr ;

existence
ex b₁ being complete strict TopLattice st
( b₁ is Lawson & b₁ is continuous )

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
for b₁, b₂ being Subset-Family of T st ( for S being correct Lawson TopAugmentation of T holds b₁ = the topology of S ) & ( for S being correct Lawson TopAugmentation of T holds b₂ = the topology of S ) holds
b₁ = b₂

proof end;

existence
ex b₁ being Subset-Family of T st
for S being correct Lawson TopAugmentation of T holds b₁ = the topology of S

proof end;

end;

:: deftheorem Def4 defines lambda WAYBEL19:def 4 :
for T being complete LATTICE
for b₂ being Subset-Family of T holds
( b₂ = lambda T iff for S being correct Lawson TopAugmentation of T holds b₂ = the topology of S );

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;

Lm2: for T being LATTICE
for F being Subset-Family of T st ( for A being Subset of T st A in F holds
A is property(S) ) holds
union F is property(S)

proof end;

Lm3: for T being LATTICE
for A1, A2 being Subset of T st A1 is property(S) & A2 is property(S) holds
A1 /\ A2 is property(S)

proof end;

Lm4: for T being LATTICE holds [#] T is 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 is 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 is property(S)

proof end;

theorem Th37: :: WAYBEL19:37

for S being complete Scott 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 complete continuous 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 complete Scott 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 TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Lawson -> T_1 complete compact for TopRelStr ;

coherence
for b₁ being complete TopLattice st b₁ is Lawson holds
( b₁ is T_1 & b₁ is compact )

proof end;

end;

registration

cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete continuous Lawson -> Hausdorff complete continuous for TopRelStr ;

coherence
for b₁ being complete continuous TopLattice st b₁ is Lawson holds
b₁ is Hausdorff

proof end;

end;