let S, T be complete Scott TopLattice; :: thesis: for f being Function of S,T holds
( f is continuous iff f is directed-sups-preserving )
let f be Function of S,T; :: thesis: ( f is continuous iff f is directed-sups-preserving )
thus ( f is continuous implies f is directed-sups-preserving ) :: thesis: ( f is directed-sups-preserving implies f is continuous )
proof
assume f is continuous ; :: thesis: f is directed-sups-preserving
then for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) by Lm9;
hence f is directed-sups-preserving by Lm8; :: thesis: verum
end;
thus ( f is directed-sups-preserving implies f is continuous ) by Lm4; :: thesis: verum