proposition: Lemma positive_imp_maps_compacts_into : forall (J : interval) F, positive_fun J F -> Continuous J F -> maps_compacts_into J (openl [0]) F.
proof: Proof. intros J F H H0 a b Hab H1. elim H; intros incF H2. elim H2; clear H H2 incF; intros MinF H H2. set (MaxF := Norm_Funct (included_imp_Continuous _ _ H0 _ _ _ H1) [+][1]) in *. cut (MinF [<] MaxF). intro H3. exists MinF; exists MaxF; exists H3. split. eapply included_trans. apply compact_map2 with (Hab' := Min_leEq_Max MinF MaxF). apply included_interval; simpl in |- *. auto. unfold MaxF in |- *; eapply leEq_less_trans. 2: apply less_plusOne. apply positive_norm. intros; split. auto. unfold MaxF in |- *; eapply leEq_transitive. 2: apply less_leEq; apply less_plusOne. eapply leEq_transitive. apply leEq_AbsIR. apply norm_bnd_AbsIR; auto. unfold MaxF in |- *; eapply leEq_less_trans. 2: apply less_plusOne. apply leEq_transitive with (F a (Continuous_imp_inc _ _ H0 _ (H1 a (compact_inc_lft _ _ Hab)))). apply H2; auto. apply H1; apply compact_inc_lft. eapply leEq_transitive. apply leEq_AbsIR. apply norm_bnd_AbsIR; apply compact_inc_lft. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries