proposition: Lemma negative_imp_maps_compacts_into : forall (J : interval) F, negative_fun J F -> Continuous J F -> maps_compacts_into J (openr [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 MaxF H H2. set (MinF := [--] (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 |- *. unfold MinF in |- *; eapply less_leEq_trans. apply minusOne_less. astepr ( [--]ZeroR); apply inv_resp_leEq; apply positive_norm. auto. intros; split. unfold MinF in |- *; eapply leEq_transitive. apply less_leEq; apply minusOne_less. astepr ( [--][--] (Part _ _ Hx)); apply inv_resp_leEq. eapply leEq_transitive. apply inv_leEq_AbsIR. apply norm_bnd_AbsIR; auto. auto. unfold MinF in |- *; eapply less_leEq_trans. apply minusOne_less. apply leEq_transitive with (F a (Continuous_imp_inc _ _ H0 _ (H1 a (compact_inc_lft _ _ Hab)))). 2: apply H2; auto. 2: apply H1; apply compact_inc_lft. astepr ( [--] [--] (Part _ _ (Continuous_imp_inc _ _ H0 _ (H1 _ (compact_inc_lft _ _ Hab))))); apply inv_resp_leEq. eapply leEq_transitive. apply inv_leEq_AbsIR. apply norm_bnd_AbsIR; apply compact_inc_lft. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries