let P, Q be non empty strict chain-complete Poset; :: thesis: for f being Function of P,Q holds
( f is continuous iff ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) ) )
let f be Function of P,Q; :: thesis: ( f is continuous iff ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) ) )
thus ( f is continuous implies ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) ) ) :: thesis: ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) implies f is continuous )
proof
assume A1: f is continuous ; :: thesis: ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) )
for L being non empty Chain of P holds f . (sup L) = sup (f .: L)
proof
let L be non empty Chain of P; :: thesis: f . (sup L) = sup (f .: L)
A2: f preserves_sup_of L by A1;
ex_sup_of L,P by Def1;
hence f . (sup L) = sup (f .: L) by A2, WAYBEL_0:def 31; :: thesis: verum
end;
hence ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) ) by A1; :: thesis: verum
end;
assume that
A3: f is monotone and
A4: for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ; :: thesis: f is continuous
for L being non empty Chain of P holds f preserves_sup_of L
proof
let L be non empty Chain of P; :: thesis: f preserves_sup_of L
reconsider M = f .: L as non empty Chain of Q by A3, Th1;
( ex_sup_of M,Q & f . (sup L) = sup M ) by Def1, A4;
hence f preserves_sup_of L by WAYBEL_0:def 31; :: thesis: verum
end;
hence f is continuous by A3; :: thesis: verum