let S, T be complete Scott TopLattice; :: thesis: for f being Function of S,T st S is algebraic & T is algebraic holds

( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) )

let f be Function of S,T; :: thesis: ( S is algebraic & T is algebraic implies ( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) )

assume that

A1: S is algebraic and

A2: T is algebraic ; :: thesis: ( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) )

A3: S is continuous by A1, WAYBEL_8:7;

A4: T is continuous by A2, WAYBEL_8:7;

then for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by Th26;

hence f is continuous by A3, A4, Th24; :: thesis: verum

( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) )

let f be Function of S,T; :: thesis: ( S is algebraic & T is algebraic implies ( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) )

assume that

A1: S is algebraic and

A2: T is algebraic ; :: thesis: ( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) )

A3: S is continuous by A1, WAYBEL_8:7;

A4: T is continuous by A2, WAYBEL_8:7;

hereby :: thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) implies f is continuous )

assume
for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)
; :: thesis: f is continuous assume
f is continuous
; :: thesis: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)

then for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by A3, A4, Th24;

hence for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) by A1, A2, Lm19; :: thesis: verum

end;then for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by A3, A4, Th24;

hence for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) by A1, A2, Lm19; :: thesis: verum

then for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by Th26;

hence f is continuous by A3, A4, Th24; :: thesis: verum