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 H1( Element of N) -> set = { (N . i) where i is Element of N : i >= $1 } ;
deffunc H2( Element of N) -> Element of the carrier of S = "/\" (H1($1),S);
defpred S1[ set ] means verum;
A6: f .: { H2(i) where i is Element of N : S1[i] } = { (f . H2(i)) where i is Element of N : S1[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 .: H1(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 .: H1(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 .: H1(j) = { ((f * N) . n) where n is Element of (f * N) : n >= j9 } )
assume A9: j9 = j ; :: thesis: f .: H1(j) = { ((f * N) . n) where n is Element of (f * N) : n >= j9 }
defpred S2[ Element of N] means $1 >= j;
defpred S3[ Element of (f * N)] means $1 >= j9;
deffunc H3( Element of N) -> Element of the carrier of T = f . (N . $1);
deffunc H4( set ) -> set = f . ( the mapping of N . $1);
A10: for v being Element of N st S2[v] holds
H3(v) = H4(v) ;
deffunc H5( set ) -> set = (f * the mapping of N) . $1;
deffunc H6( Element of (f * N)) -> Element of the carrier of T = (f * N) . $1;
A11: for v being Element of N st S2[v] holds
H4(v) = H5(v) by FUNCT_2:15;
A12: for v being Element of (f * N) st S3[v] holds
H5(v) = H6(v) by WAYBEL_9:def 8;
defpred S4[ set ] means [j9,$1] in the InternalRel of N;
A13: for v being Element of N holds
( S2[v] iff S4[v] ) by A9, ORDERS_2:def 5;
A14: for v being Element of (f * N) holds
( S4[v] iff S3[v] ) by A4, ORDERS_2:def 5;
deffunc H7( Element of N) -> Element of the carrier of S = N . $1;
thus f .: H1(j) = f .: { H7(i) where i is Element of N : S2[i] }
.= { (f . H7(k)) where k is Element of N : S2[k] } from LATTICE3:sch 2(A5)
.= { H3(k) where k is Element of N : S2[k] }
.= { H4(s) where s is Element of N : S2[s] } from FRAENKEL:sch 6(A10)
.= { H5(o) where o is Element of N : S2[o] } from FRAENKEL:sch 6(A11)
.= { H5(r) where r is Element of N : S4[r] } from FRAENKEL:sch 3(A13)
.= { H5(m) where m is Element of (f * N) : S4[m] } by A4
.= { H5(q) where q is Element of (f * N) : S3[q] } from FRAENKEL:sch 3(A14)
.= { H6(n) where n is Element of (f * N) : S3[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 . ("/\" (H1(j),S)) = "/\" ((f .: H1(j)),T)
let j be Element of N; :: thesis: f . ("/\" (H1(j),S)) = "/\" ((f .: H1(j)),T)
H1(j) c= the carrier of S
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in H1(j) or b in the carrier of S )
assume b in H1(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 = H1(j) as Subset of S ;
A16: f preserves_inf_of A by A1;
ex_inf_of A,S by YELLOW_0:17;
hence f . ("/\" (H1(j),S)) = "/\" ((f .: H1(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 .: H1(j)),T) by A15, A17;
reconsider j9 = j as Element of (f * N) by A4;
f .: H1(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 .: H1(j)),T) by A8, A19
.= f . ("/\" (H1(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