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 )

( 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

thus
( f is directed-sups-preserving implies f is continuous )
by Lm4; :: thesis: verum
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;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