:: Lawson Topology in Continuous Lattices
:: by Grzegorz Bancerek
::
:: Received July 12, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

definition
let S, T be Semilattice;
assume B1: ( S is upper-bounded implies T is upper-bounded ) ;
mode SemilatticeHomomorphism of S,T ->  Function of S,T means :Def1: :: WAYBEL21:def 1
 for X being finite Subset of S holds it preserves_inf_of X;
existence
 ex b1 being Function of S,T st
for X being finite Subset of S holds b1 preserves_inf_of X
proofend;
end;

:: deftheorem Def1 defines SemilatticeHomomorphism WAYBEL21:def_1_:_
 for S, T being Semilattice st ( S is upper-bounded implies T is upper-bounded ) holds
for b3 being Function of S,T holds
( b3 is SemilatticeHomomorphism of S,T iff for X being finite Subset of S holds b3 preserves_inf_of X );

registration
let S, T be Semilattice;
cluster Function-like V29( the carrier of S, the carrier of T) meet-preserving  ->  monotone for Element of K22(K23( the carrier of S, the carrier of T));
coherence
 for b1 being Function of S,T st b1 is meet-preserving holds
b1 is monotone
proofend;
end;

registration
let S be Semilattice;
let T be upper-bounded Semilattice;
cluster  ->  meet-preserving for SemilatticeHomomorphism of S,T;
coherence
 for b1 being SemilatticeHomomorphism of S,T holds b1 is meet-preserving
proofend;
end;

theorem :: WAYBEL21:1
for S, T being upper-bounded Semilattice
for f being SemilatticeHomomorphism of S,T holds f . (Top S) = Top T
proofend;

theorem Th2: :: WAYBEL21:2
for S, T being Semilattice
for f being Function of S,T st f is meet-preserving holds
for X being non empty finite Subset of S holds f preserves_inf_of X
proofend;

theorem :: WAYBEL21:3
for S, T being upper-bounded Semilattice
for f being meet-preserving Function of S,T st f . (Top S) = Top T holds
f is SemilatticeHomomorphism of S,T
proofend;

theorem Th4: :: WAYBEL21:4
for S, T being Semilattice
for f being Function of S,T st f is meet-preserving & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds
for X being non empty Subset of S holds f preserves_inf_of X
proofend;

theorem Th5: :: WAYBEL21:5
for S, T being Semilattice
for f being Function of S,T st f is infs-preserving holds
f is SemilatticeHomomorphism of S,T
proofend;

theorem Th6: :: WAYBEL21:6
for S1, T1, S2, T2 being non empty RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds
for f1 being Function of S1,T1
for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is infs-preserving implies f2 is infs-preserving ) & ( f1 is directed-sups-preserving implies f2 is directed-sups-preserving ) )
proofend;

theorem :: WAYBEL21:7
for S1, T1, S2, T2 being non empty RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds
for f1 being Function of S1,T1
for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) )
proofend;

theorem Th8: :: WAYBEL21:8
for T being complete LATTICE
for S being non empty full infs-inheriting SubRelStr of T holds incl (S,T) is infs-preserving
proofend;

theorem :: WAYBEL21:9
for T being complete LATTICE
for S being non empty full sups-inheriting SubRelStr of T holds incl (S,T) is sups-preserving
proofend;

theorem Th10: :: WAYBEL21:10
for T being non empty up-complete Poset
for S being non empty full directed-sups-inheriting SubRelStr of T holds incl (S,T) is directed-sups-preserving
proofend;

theorem :: WAYBEL21:11
for T being complete LATTICE
for S being non empty full filtered-infs-inheriting SubRelStr of T holds incl (S,T) is filtered-infs-preserving
proofend;

theorem Th12: :: WAYBEL21:12
for T1, T2, R being RelStr
for S being SubRelStr of T1 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) holds
( R is SubRelStr of T2 & ( S is full implies R is full SubRelStr of T2 ) )
proofend;

theorem Th13: :: WAYBEL21:13
for T being non empty RelStr holds T is full infs-inheriting sups-inheriting SubRelStr of T
proofend;

registration
let T be complete LATTICE;
cluster non empty reflexive transitive antisymmetric full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting with_infima complete for SubRelStr of T;
existence
 ex b1 being CLSubFrame of T st b1 is complete
proofend;
end;

theorem Th14: :: WAYBEL21:14
for T being Semilattice
for S being non empty full SubRelStr of T holds
( S is meet-inheriting iff for X being non empty finite Subset of S holds "/\" (X,T) in the carrier of S )
proofend;

theorem Th15: :: WAYBEL21:15
for T being sup-Semilattice
for S being non empty full SubRelStr of T holds
( S is join-inheriting iff for X being non empty finite Subset of S holds "\/" (X,T) in the carrier of S )
proofend;

theorem Th16: :: WAYBEL21:16
for T being upper-bounded Semilattice
for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & S is filtered-infs-inheriting holds
S is infs-inheriting
proofend;

theorem :: WAYBEL21:17
for T being lower-bounded sup-Semilattice
for S being non empty full join-inheriting SubRelStr of T st Bottom T in the carrier of S & S is directed-sups-inheriting holds
S is sups-inheriting
proofend;

theorem Th18: :: WAYBEL21:18
for T being complete LATTICE
for S being non empty full SubRelStr of T st S is infs-inheriting holds
S is complete
proofend;

theorem :: WAYBEL21:19
for T being complete LATTICE
for S being non empty full SubRelStr of T st S is sups-inheriting holds
S is complete
proofend;

theorem :: WAYBEL21:20
for T1, T2 being non empty RelStr
for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is infs-inheriting holds
S2 is infs-inheriting
proofend;

theorem :: WAYBEL21:21
for T1, T2 being non empty RelStr
for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is sups-inheriting holds
S2 is sups-inheriting
proofend;

theorem :: WAYBEL21:22
for T1, T2 being non empty RelStr
for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is directed-sups-inheriting holds
S2 is directed-sups-inheriting
proofend;

theorem :: WAYBEL21:23
for T1, T2 being non empty RelStr
for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is filtered-infs-inheriting holds
S2 is filtered-infs-inheriting
proofend;

begin

theorem Th24: :: WAYBEL21:24
for S, T being non empty TopSpace
for N being net of S
for f being Function of S,T st f is continuous holds
f .: (Lim N) c= Lim (f * N)
proofend;

definition
let T be non empty RelStr ;
let N be non empty NetStr over T;
redefine attr N is antitone  means :Def2: :: WAYBEL21:def 2
 for i, j being Element of N st i <= j holds
N . i >= N . j;
compatibility
 ( N is antitone iff for i, j being Element of N st i <= j holds
N . i >= N . j )
proofend;
end;

:: deftheorem Def2 defines antitone WAYBEL21:def_2_:_
 for T being non empty RelStr
for N being non empty NetStr over T holds
( N is antitone iff for i, j being Element of N st i <= j holds
N . i >= N . j );

registration
let T be non empty reflexive RelStr ;
let x be Element of T;
cluster{x} opp+id  ->  transitive directed monotone antitone ;
coherence
 ( {x} opp+id is transitive &amp; {x} opp+id is directed &amp; {x} opp+id is monotone &amp; {x} opp+id is antitone )
proofend;
end;

registration
let T be non empty reflexive RelStr ;
cluster non empty reflexive transitive strict directed monotone antitone for NetStr over T;
existence
 ex b1 being net of T st
( b1 is monotone &amp; b1 is antitone &amp; b1 is reflexive &amp; b1 is strict )
proofend;
end;

registration
let T be non empty RelStr ;
let F be non empty Subset of T;
clusterF opp+id  ->  antitone ;
coherence
 F opp+id is antitone
proofend;
end;

registration
let S, T be non empty reflexive RelStr ;
let f be monotone Function of S,T;
let N be non empty antitone NetStr over S;
clusterf * N ->  antitone ;
coherence
 f * N is antitone
proofend;
end;

theorem Th25: :: WAYBEL21:25
for S being complete LATTICE
for N being net of S holds  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  is non empty directed Subset of S
proofend;

theorem :: WAYBEL21:26
for S being non empty Poset
for N being reflexive monotone net of S holds  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,S)) where j is Element of N : verum  }  is non empty directed Subset of S
proofend;

theorem Th27: :: WAYBEL21:27
for S being non empty 1-sorted
for N being non empty NetStr over S
for X being set st rng the mapping of N c= X holds
N is_eventually_in X
proofend;

theorem Th28: :: WAYBEL21:28
for R being non empty /\-complete Poset
for F being non empty filtered Subset of R holds lim_inf (F opp+id) = inf F
proofend;

theorem Th29: :: WAYBEL21:29
for S, T being non empty /\-complete Poset
for X being non empty filtered Subset of S
for f being monotone Function of S,T holds lim_inf (f * (X opp+id)) = inf (f .: X)
proofend;

theorem Th30: :: WAYBEL21:30
for S, T being non empty TopPoset
for X being non empty filtered Subset of S
for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f .: X holds
f * (X opp+id) is subnet of Y opp+id
proofend;

theorem :: WAYBEL21:31
for S, T being non empty TopPoset
for X being non empty filtered Subset of S
for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f .: X holds
Lim (Y opp+id) c= Lim (f * (X opp+id))
proofend;

theorem Th32: :: WAYBEL21:32
for S being non empty reflexive RelStr
for D being non empty Subset of S holds
( the mapping of (Net-Str D) = id D &amp; the carrier of (Net-Str D) = D &amp; Net-Str D is full SubRelStr of S )
proofend;

theorem Th33: :: WAYBEL21:33
for S, T being non empty up-complete Poset
for f being monotone Function of S,T
for D being non empty directed Subset of S holds lim_inf (f * (Net-Str D)) = sup (f .: D)
proofend;

theorem Th34: :: WAYBEL21:34
for S being non empty reflexive RelStr
for D being non empty directed Subset of S
for i, j being Element of (Net-Str D) holds
( i <= j iff (Net-Str D) . i <= (Net-Str D) . j )
proofend;

theorem Th35: :: WAYBEL21:35
for T being complete Lawson TopLattice
for D being non empty directed Subset of T holds sup D in Lim (Net-Str D)
proofend;

definition
let T be non empty 1-sorted ;
let N be net of T;
let M be non empty NetStr over T;
assume A1: M is subnet of N ;
mode Embedding of M,N ->  Function of M,N means :Def3: :: WAYBEL21:def 3
( the mapping of M = the mapping of N * it &amp; ( for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= it . p ) );
existence
 ex b1 being Function of M,N st
( the mapping of M = the mapping of N * b1 &amp; ( for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= b1 . p ) ) by A1, YELLOW_6:def_9;
end;

:: deftheorem Def3 defines Embedding WAYBEL21:def_3_:_
 for T being non empty 1-sorted
for N being net of T
for M being non empty NetStr over T st M is subnet of N holds
for b4 being Function of M,N holds
( b4 is Embedding of M,N iff ( the mapping of M = the mapping of N * b4 &amp; ( for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= b4 . p ) ) );

theorem Th36: :: WAYBEL21:36
for T being non empty 1-sorted
for N being net of T
for M being subnet of N
for e being Embedding of M,N
for i being Element of M holds M . i = N . (e . i)
proofend;

theorem Th37: :: WAYBEL21:37
for T being complete LATTICE
for N being net of T
for M being subnet of N holds lim_inf N <= lim_inf M
proofend;

theorem Th38: :: WAYBEL21:38
for T being complete LATTICE
for N being net of T
for M being subnet of N
for e being Embedding of M,N st ( for i being Element of N
for j being Element of M st e . j <= i holds
ex j9 being Element of M st
( j9 >= j &amp; N . i >= M . j9 ) ) holds
lim_inf N = lim_inf M
proofend;

theorem :: WAYBEL21:39
for T being non empty RelStr
for N being net of T
for M being non empty full SubNetStr of N st ( for i being Element of N ex j being Element of N st
( j >= i &amp; j in the carrier of M ) ) holds
( M is subnet of N &amp; incl (M,N) is Embedding of M,N )
proofend;

theorem Th40: :: WAYBEL21:40
for T being non empty RelStr
for N being net of T
for i being Element of N holds
( N | i is subnet of N &amp; incl ((N | i),N) is Embedding of N | i,N )
proofend;

theorem Th41: :: WAYBEL21:41
for T being complete LATTICE
for N being net of T
for i being Element of N holds lim_inf (N | i) = lim_inf N
proofend;

theorem Th42: :: WAYBEL21:42
for T being non empty RelStr
for N being net of T
for X being set st N is_eventually_in X holds
ex i being Element of N st
( N . i in X &amp; rng the mapping of (N | i) c= X )
proofend;

theorem Th43: :: WAYBEL21:43
for T being complete Lawson TopLattice
for N being eventually-filtered net of T holds rng the mapping of N is non empty filtered Subset of T
proofend;

theorem Th44: :: WAYBEL21:44
for T being complete Lawson TopLattice
for N being eventually-filtered net of T holds Lim N = {(inf N)}
proofend;

begin

theorem Th45: :: WAYBEL21:45
for S, T being complete Lawson TopLattice
for f being meet-preserving Function of S,T holds
( f is continuous iff ( f is directed-sups-preserving &amp; ( for X being non empty Subset of S holds f preserves_inf_of X ) ) )
proofend;

theorem Th46: :: WAYBEL21:46
for S, T being complete Lawson TopLattice
for f being SemilatticeHomomorphism of S,T holds
( f is continuous iff ( f is infs-preserving &amp; f is directed-sups-preserving ) )
proofend;

definition
let S, T be non empty RelStr ;
let f be Function of S,T;
attrf is lim_infs-preserving  means :: WAYBEL21:def 4
 for N being net of S holds f . (lim_inf N) = lim_inf (f * N);
end;

:: deftheorem  defines lim_infs-preserving WAYBEL21:def_4_:_
 for S, T being non empty RelStr
for f being Function of S,T holds
( f is lim_infs-preserving iff for N being net of S holds f . (lim_inf N) = lim_inf (f * N) );

theorem :: WAYBEL21:47
for S, T being complete Lawson TopLattice
for f being SemilatticeHomomorphism of S,T holds
( f is continuous iff f is lim_infs-preserving )
proofend;

theorem Th48: :: WAYBEL21:48
for T being continuous complete Lawson TopLattice
for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S &amp; ex X being Subset of T st
( X = the carrier of S &amp; X is closed ) holds
S is infs-inheriting
proofend;

theorem Th49: :: WAYBEL21:49
for T being continuous complete Lawson TopLattice
for S being non empty full SubRelStr of T st ex X being Subset of T st
( X = the carrier of S &amp; X is closed ) holds
S is directed-sups-inheriting
proofend;

theorem Th50: :: WAYBEL21:50
for T being continuous complete Lawson TopLattice
for S being non empty full infs-inheriting directed-sups-inheriting SubRelStr of T ex X being Subset of T st
( X = the carrier of S &amp; X is closed )
proofend;

theorem Th51: :: WAYBEL21:51
for T being continuous complete Lawson TopLattice
for S being non empty full infs-inheriting directed-sups-inheriting SubRelStr of T
for N being net of T st N is_eventually_in the carrier of S holds
lim_inf N in the carrier of S
proofend;

theorem Th52: :: WAYBEL21:52
for T being continuous complete Lawson TopLattice
for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S &amp; ( for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ) holds
S is infs-inheriting
proofend;

theorem Th53: :: WAYBEL21:53
for T being continuous complete Lawson TopLattice
for S being non empty full SubRelStr of T st ( for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ) holds
S is directed-sups-inheriting
proofend;

theorem :: WAYBEL21:54
for T being continuous complete Lawson TopLattice
for S being non empty full meet-inheriting SubRelStr of T
for X being Subset of T st X = the carrier of S &amp; Top T in X holds
( X is closed iff for N being net of T st N is_eventually_in X holds
lim_inf N in X )
proofend;