let S, T be complete Lawson TopLattice; :: thesis: for f being SemilatticeHomomorphism of S,T holds
( f is continuous iff ( f is infs-preserving & f is directed-sups-preserving ) )
let f be SemilatticeHomomorphism of S,T; :: thesis: ( f is continuous iff ( f is infs-preserving & f is directed-sups-preserving ) )
hereby :: thesis: ( f is infs-preserving & f is directed-sups-preserving implies f is continuous )
assume A1: f is continuous ; :: thesis: ( f is infs-preserving & f is directed-sups-preserving )
A2: for X being finite Subset of S holds f preserves_inf_of X by Def1;
for X being non empty filtered Subset of S holds f preserves_inf_of X by A1, Th45;
hence f is infs-preserving by A2, WAYBEL_0:71; :: thesis: f is directed-sups-preserving
thus f is directed-sups-preserving by A1, Th45; :: thesis: verum
end;
assume f is infs-preserving ; :: thesis: ( not f is directed-sups-preserving or f is continuous )
then for X being non empty Subset of S holds f preserves_inf_of X ;
hence ( not f is directed-sups-preserving or f is continuous ) by Th45; :: thesis: verum