:: 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 b1 being 1 -element TopSpace-like reflexive TopRelStr holds b1 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 b1 being TopLattice st
( b1 is lower & b1 is trivial & b1 is complete & b1 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 b1 being correct strict TopAugmentation of R st b1 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 b1, b2 being Subset-Family of R st ( for T being correct lower TopAugmentation of R holds b1 = the topology of T ) & ( for T being correct lower TopAugmentation of R holds b2 = the topology of T ) holds
b1 = b2
proof end;
existence
ex b1 being Subset-Family of R st
for T being correct lower TopAugmentation of R holds b1 = the topology of T
proof end;
end;

:: deftheorem Def2 defines omega WAYBEL19:def 2 :
for R being non empty RelStr
for b2 being Subset-Family of R holds
( b2 = omega R iff for T being correct lower TopAugmentation of R holds b2 = 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 b1 being non empty TopPoset st b1 is lower holds
b1 is T_0
proof end;
end;

registration
let R be non empty lower-bounded RelStr ;
cluster -> lower-bounded for TopAugmentation of R;
coherence
for b1 being TopAugmentation of R holds b1 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{ F1() -> TopLattice, P1[ set ] } :
for A being Subset of F1() st A is open holds
P1[A]
provided
A1: ex K being prebasis of F1() st
for A being Subset of F1() st A in K holds
P1[A] and
A2: for F being Subset-Family of F1() st ( for A being Subset of F1() st A in F holds
P1[A] ) holds
P1[ union F] and
A3: for A1, A2 being Subset of F1() st P1[A1] & P1[A2] holds
P1[A1 /\ A2] and
A4: P1[ [#] F1()]
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 b1 being TopAugmentation of T holds b1 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 b1 being TopAugmentation of R st
( b1 is Lawson & b1 is strict & b1 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 b1 being TopLattice st
( b1 is Scott & b1 is complete & b1 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 b1 being complete strict TopLattice st
( b1 is Lawson & b1 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 b1, b2 being Subset-Family of T st ( for S being correct Lawson TopAugmentation of T holds b1 = the topology of S ) & ( for S being correct Lawson TopAugmentation of T holds b2 = the topology of S ) holds
b1 = b2
proof end;
existence
ex b1 being Subset-Family of T st
for S being correct Lawson TopAugmentation of T holds b1 = the topology of S
proof end;
end;

:: deftheorem Def4 defines lambda WAYBEL19:def 4 :
for T being complete LATTICE
for b2 being Subset-Family of T holds
( b2 = lambda T iff for S being correct Lawson TopAugmentation of T holds b2 = 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 b1 being complete TopLattice st b1 is Lawson holds
( b1 is T_1 & b1 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 b1 being complete continuous TopLattice st b1 is Lawson holds
b1 is Hausdorff
proof end;
end;