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


begin

definition
let T be non empty TopRelStr ;
attrT 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 toTARSKI: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 set ; ::_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 set ; :: according toTARSKI: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
cluster1 -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
proofend;
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 )
proofend;
end;

theorem Th1: :: WAYBEL19:1
for LL being non empty RelStr ex T being correct strict TopAugmentation of LL st T is lower
proofend;

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
proofend;

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
proofend;
existence
 ex b1 being Subset-Family of R st
for T being correct lower TopAugmentation of R holds b1 = the topology of T
proofend;
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
proofend;

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 )
proofend;

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
proofend;

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
proofend;

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 )
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;
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
proofend;
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) `):]
proofend;

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:]
proofend;

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

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
proofend;

begin

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()]
proofend;

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
proofend;

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
proofend;
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
proofend;

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
proofend;

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
proofend;

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 ) )
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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 )
proofend;

theorem Th28: :: WAYBEL19:28
for R being non empty reflexive antisymmetric RelStr
for x being Element of R holds (uparrow x) /\ (downarrow x) = {x}
proofend;

begin

definition
let T be non empty reflexive TopRelStr ;
attrT 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 )
proofend;

registration
let R be complete LATTICE;
cluster non empty correct reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() 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 )
proofend;
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 )
proofend;
cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() continuous up-complete /\-complete strict non void Lawson for TopRelStr ;
existence
 ex b1 being complete strict TopLattice st
( b1 is Lawson & b1 is continuous )
proofend;
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
proofend;

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
proofend;

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
proofend;

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
proofend;
existence
 ex b1 being Subset-Family of T st
for S being correct Lawson TopAugmentation of T holds b1 = the topology of S
proofend;
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)))
proofend;

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
proofend;

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)
proofend;

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)
proofend;

Lm4:  for T being LATTICE holds [#] T is property(S)
proofend;

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)
proofend;

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)
proofend;

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
proofend;

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 )
proofend;

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 )
proofend;

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 )
proofend;

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
proofend;

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 )
proofend;

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)}
proofend;

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 )
proofend;
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
proofend;
end;