let S, T be complete Lawson TopLattice; :: thesis: for f being SemilatticeHomomorphism of S,T holds
( f is continuous iff f is lim_infs-preserving )
let f be SemilatticeHomomorphism of S,T; :: thesis: ( f is continuous iff f is lim_infs-preserving )
thus ( f is continuous implies f is lim_infs-preserving ) :: thesis: ( f is lim_infs-preserving implies f is continuous )

proof

assume f is continuous ; :: thesis: f is lim_infs-preserving
then A1: ( f is infs-preserving & f is directed-sups-preserving ) by Th46;
let N be net of S; :: according to WAYBEL21:def 4 :: thesis: f . (lim_inf N) = lim_inf (f * N)
set M = f * N;
set Y = { ("/\" { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T) where j is Element of (f * N) : verum } ;
reconsider X = { ("/\" { (N . i) where i is Element of N : i >= j } ,S) where j is Element of N : verum } as non empty directed Subset of S by Th25;
A2: ( ex_sup_of X,S & f preserves_sup_of X ) by A1, WAYBEL_0:def 37, YELLOW_0:17;
A3: ( the mapping of (f * N) = f * the mapping of N & RelStr(# the carrier of (f * N),the InternalRel of (f * N) #) = RelStr(# the carrier of N,the InternalRel of N #) ) by WAYBEL_9:def 8;
A4: the carrier of S c= dom f by FUNCT_2:def 1;
deffunc H₁( Element of N) -> set = { (N . i) where i is Element of N : i >= $1 } ;
deffunc H₂( Element of N) -> Element of the carrier of S = "/\" H₁($1),S;
defpred S₁[ set ] means verum;
A5: f .: { H₂(i) where i is Element of N : S₁[i] } = { (f . H₂(i)) where i is Element of N : S₁[i] } from LATTICE3:sch 2(A4);
A6: f .: X = { ("/\" { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T) where j is Element of (f * N) : verum }

proof

A7: now

let j be Element of N; :: thesis: for j' being Element of (f * N) st j' = j holds
f .: H₁(j) = { ((f * N) . n) where n is Element of (f * N) : n >= j' }
let j' be Element of (f * N); :: thesis: ( j' = j implies f .: H₁(j) = { ((f * N) . n) where n is Element of (f * N) : n >= j' } )
assume A8: j' = j ; :: thesis: f .: H₁(j) = { ((f * N) . n) where n is Element of (f * N) : n >= j' }
defpred S₂[ Element of N] means $1 >= j;
defpred S₃[ Element of (f * N)] means $1 >= j';
deffunc H₃( Element of N) -> Element of the carrier of T = f . (N . $1);
deffunc H₄( set ) -> set = f . (the mapping of N . $1);
A9: for v being Element of N st S₂[v] holds
H₃(v) = H₄(v) ;
deffunc H₅( set ) -> set = (f * the mapping of N) . $1;
deffunc H₆( Element of (f * N)) -> Element of the carrier of T = (f * N) . $1;
A10: for v being Element of N st S₂[v] holds
H₄(v) = H₅(v) by FUNCT_2:21;
A11: for v being Element of (f * N) st S₃[v] holds
H₅(v) = H₆(v) by WAYBEL_9:def 8;
defpred S₄[ set ] means [j',$1] in the InternalRel of N;
A12: for v being Element of N holds
( S₂[v] iff S₄[v] ) by A8, ORDERS_2:def 9;
A13: for v being Element of (f * N) holds
( S₄[v] iff S₃[v] ) by A3, ORDERS_2:def 9;
deffunc H₇( Element of N) -> Element of the carrier of S = N . $1;
thus f .: H₁(j) = f .: { H₇(i) where i is Element of N : S₂[i] }
.= { (f . H₇(k)) where k is Element of N : S₂[k] } from LATTICE3:sch 2(A4)
.= { H₃(k) where k is Element of N : S₂[k] }
.= { H₄(s) where s is Element of N : S₂[s] } from FRAENKEL:sch 6(A9)
.= { H₅(o) where o is Element of N : S₂[o] } from FRAENKEL:sch 6(A10)
.= { H₅(r) where r is Element of N : S₄[r] } from FRAENKEL:sch 3(A12)
.= { H₅(m) where m is Element of (f * N) : S₄[m] } by A3
.= { H₅(q) where q is Element of (f * N) : S₃[q] } from FRAENKEL:sch 3(A13)
.= { H₆(n) where n is Element of (f * N) : S₃[n] } from FRAENKEL:sch 6(A11)
.= { ((f * N) . n) where n is Element of (f * N) : n >= j' } ; :: thesis: verum

end;

A14: now

let j be Element of N; :: thesis: f . ("/\" H₁(j),S) = "/\" (f .: H₁(j)),T
H₁(j) c= the carrier of S

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in H₁(j) or b in the carrier of S )
assume b in H₁(j) ; :: thesis: b in the carrier of S
then ex i being Element of N st
( b = N . i & i >= j ) ;
hence b in the carrier of S ; :: thesis: verum

end;

then reconsider A = H₁(j) as Subset of S ;
( f preserves_inf_of A & ex_inf_of A,S ) by A1, WAYBEL_0:def 32, YELLOW_0:17;
hence f . ("/\" H₁(j),S) = "/\" (f .: H₁(j)),T by WAYBEL_0:def 30; :: thesis: verum

end;

thus f .: X c= { ("/\" { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T) where j is Element of (f * N) : verum } :: according to XBOOLE_0:def 10 :: thesis: { ("/\" { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T) where j is Element of (f * N) : verum } c= f .: X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in f .: X or a in { ("/\" { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T) where j is Element of (f * N) : verum } )
assume a in f .: X ; :: thesis: a in { ("/\" { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T) where j is Element of (f * N) : verum }
then consider j being Element of N such that
A15: a = f . ("/\" { (N . i) where i is Element of N : i >= j } ,S) by A5;
A16: a = "/\" (f .: H₁(j)),T by A14, A15;
reconsider j' = j as Element of (f * N) by A3;
f .: H₁(j) = { ((f * N) . n) where n is Element of (f * N) : n >= j' } by A7;
hence a in { ("/\" { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T) where j is Element of (f * N) : verum } by A16; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { ("/\" { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T) where j is Element of (f * N) : verum } or a in f .: X )
assume a in { ("/\" { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T) where j is Element of (f * N) : verum } ; :: thesis: a in f .: X
then consider j' being Element of (f * N) such that
A17: a = "/\" { ((f * N) . n) where n is Element of (f * N) : n >= j' } ,T ;
reconsider j = j' as Element of N by A3;
a = "/\" (f .: H₁(j)),T by A7, A17
.= f . ("/\" H₁(j),S) by A14 ;
hence a in f .: X by A5; :: thesis: verum

end;

thus f . (lim_inf N) = f . (sup X) by WAYBEL11:def 6
.= sup (f .: X) by A2, WAYBEL_0:def 31
.= lim_inf (f * N) by A6, WAYBEL11:def 6 ; :: thesis: verum

end;

assume A18: for N being net of S holds f . (lim_inf N) = lim_inf (f * N) ; :: according to WAYBEL21:def 4 :: thesis: f is continuous
A19: f is directed-sups-preserving

proof

let D be Subset of S; :: according to WAYBEL_0:def 37 :: thesis: ( D is empty or not D is directed or f preserves_sup_of D )
assume ( not D is empty & D is directed ) ; :: thesis: f preserves_sup_of D
then reconsider D' = D as non empty directed Subset of S ;
assume ex_sup_of D,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of f .: D,T & "\/" (f .: D),T = f . ("\/" D,S) )
thus ex_sup_of f .: D,T by YELLOW_0:17; :: thesis: "\/" (f .: D),T = f . ("\/" D,S)
thus f . (sup D) = f . (lim_inf (Net-Str D')) by WAYBEL17:10
.= lim_inf (f * (Net-Str D')) by A18
.= sup (f .: D) by Th33 ; :: thesis: verum

end;

A20: for X being finite Subset of S holds f preserves_inf_of X by Def1;

now

let X be non empty filtered Subset of S; :: thesis: f preserves_inf_of X
reconsider fX = f .: X as non empty filtered Subset of T by WAYBEL20:25;
thus f preserves_inf_of X :: thesis: verum

proof

assume ex_inf_of X,S ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of f .: X,T & "/\" (f .: X),T = f . ("/\" X,S) )
thus ex_inf_of f .: X,T by YELLOW_0:17; :: thesis: "/\" (f .: X),T = f . ("/\" X,S)
f . (inf X) = f . (lim_inf (X opp+id )) by Th28
.= lim_inf (f * (X opp+id )) by A18
.= inf fX by Th29
.= lim_inf (fX opp+id ) by Th28 ;
hence "/\" (f .: X),T = f . ("/\" X,S) by Th28; :: thesis: verum

end;

end;

then f is infs-preserving by A20, WAYBEL_0:71;
hence f is continuous by A19, Th46; :: thesis: verum