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 by YELLOW_0:17;
A3: f preserves_sup_of X by A1;
A4: 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;
A5: 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;
A6: 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(A5);
A7: f .: X = { ("/\" ( { ((f * N) . i) where i is Element of (f * N) : i >= j } ,T)) where j is Element of (f * N) : verum }

proof

A8: now :: thesis: for j being Element of N
for j9 being Element of (f * N) st j9 = j holds
f .: H₁(j) = { ((f * N) . n) where n is Element of (f * N) : n >= j9 }

let j be Element of N; :: thesis: for j9 being Element of (f * N) st j9 = j holds
f .: H₁(j) = { ((f * N) . n) where n is Element of (f * N) : n >= j9 }
let j9 be Element of (f * N); :: thesis: ( j9 = j implies f .: H₁(j) = { ((f * N) . n) where n is Element of (f * N) : n >= j9 } )
assume A9: j9 = j ; :: thesis: f .: H₁(j) = { ((f * N) . n) where n is Element of (f * N) : n >= j9 }
defpred S₂[ Element of N] means $1 >= j;
defpred S₃[ Element of (f * N)] means $1 >= j9;
deffunc H₃( Element of N) -> Element of the carrier of T = f . (N . $1);
deffunc H₄( set ) -> set = f . ( the mapping of N . $1);
A10: 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;
A11: for v being Element of N st S₂[v] holds
H₄(v) = H₅(v) by FUNCT_2:15;
A12: for v being Element of (f * N) st S₃[v] holds
H₅(v) = H₆(v) by WAYBEL_9:def 8;
defpred S₄[ set ] means [j9,$1] in the InternalRel of N;
A13: for v being Element of N holds
( S₂[v] iff S₄[v] ) by A9, ORDERS_2:def 5;
A14: for v being Element of (f * N) holds
( S₄[v] iff S₃[v] ) by A4, ORDERS_2:def 5;
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(A5)
.= { H₃(k) where k is Element of N : S₂[k] }
.= { H₄(s) where s is Element of N : S₂[s] } from FRAENKEL:sch 6(A10)
.= { H₅(o) where o is Element of N : S₂[o] } from FRAENKEL:sch 6(A11)
.= { H₅(r) where r is Element of N : S₄[r] } from FRAENKEL:sch 3(A13)
.= { H₅(m) where m is Element of (f * N) : S₄[m] } by A4
.= { H₅(q) where q is Element of (f * N) : S₃[q] } from FRAENKEL:sch 3(A14)
.= { H₆(n) where n is Element of (f * N) : S₃[n] } from FRAENKEL:sch 6(A12)
.= { ((f * N) . n) where n is Element of (f * N) : n >= j9 } ; :: thesis: verum

end;

A15: now :: thesis: for j being Element of N holds f . ("/\" (H₁(j),S)) = "/\" ((f .: H₁(j)),T)

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 object ; :: 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 ;
A16: f preserves_inf_of A by A1;
ex_inf_of A,S by YELLOW_0:17;
hence f . ("/\" (H₁(j),S)) = "/\" ((f .: H₁(j)),T) by A16; :: 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 object ; :: 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
A17: a = f . ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) by A6;
A18: a = "/\" ((f .: H₁(j)),T) by A15, A17;
reconsider j9 = j as Element of (f * N) by A4;
f .: H₁(j) = { ((f * N) . n) where n is Element of (f * N) : n >= j9 } by A8;
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 A18; :: thesis: verum

end;

let a be object ; :: 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 j9 being Element of (f * N) such that
A19: a = "/\" ( { ((f * N) . n) where n is Element of (f * N) : n >= j9 } ,T) ;
reconsider j = j9 as Element of N by A4;
a = "/\" ((f .: H₁(j)),T) by A8, A19
.= f . ("/\" (H₁(j),S)) by A15 ;
hence a in f .: X by A6; :: thesis: verum

end;

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

end;

assume A20: for N being net of S holds f . (lim_inf N) = lim_inf (f * N) ; :: according to WAYBEL21:def 4 :: thesis: f is continuous
A21: 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 D9 = 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 D9)) by WAYBEL17:10
.= lim_inf (f * (Net-Str D9)) by A20
.= sup (f .: D) by Th33 ; :: thesis: verum

end;

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

now :: thesis: for X being non empty filtered Subset of S holds f preserves_inf_of X

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:24;
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 A20
.= 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 A22, WAYBEL_0:71;
hence f is continuous by A21, Th46; :: thesis: verum