proposition: Lemma Continuous_I_imp_lub : {x : IR | fun_lub_IR F I x}.
proof: Proof. unfold fun_lub_IR in |- *. apply totally_bounded_has_lub. apply Continuous_I_imp_tb_image. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac