proposition: Lemma Continuous_imp_maps_compacts_into : forall J F, Continuous J F -> maps_compacts_into J realline F.
proof: Proof. intros J F H a b Hab H0. set (ModF := Norm_Funct (included_imp_Continuous _ _ H _ _ _ H0)) in *. cut ( [--]ModF [<] ModF[+][1]). intro H1. exists ( [--]ModF); exists (ModF[+][1]); exists H1; split. repeat split. intros; unfold ModF in |- *; split. astepr ( [--][--] (Part _ _ Hx)); apply inv_resp_leEq. eapply leEq_transitive; [ apply inv_leEq_AbsIR | apply norm_bnd_AbsIR ]; auto. eapply leEq_transitive. 2: apply less_leEq; apply less_plusOne. eapply leEq_transitive; [ apply leEq_AbsIR | apply norm_bnd_AbsIR ]; auto. unfold ModF in |- *. eapply leEq_less_trans; [ apply leEq_transitive with ZeroR | apply less_plusOne ]. astepr ( [--]ZeroR); apply inv_resp_leEq; apply positive_norm. apply positive_norm. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries