proposition: Lemma Weak_IVT : forall I F, Continuous I F -> forall a b Ha Hb (HFab : F a Ha [<] F b Hb), I a -> I b -> forall e, [0] [<] e -> forall y, Compact (less_leEq _ _ _ HFab) y -> {x : IR | Compact (Min_leEq_Max a b) x | forall Hx, AbsIR (F x Hx[-]y) [<=] e}.
proof: Proof. intros I F H a b Ha Hb HFab H0 H1 e H2 y H3. set (H5 := less_imp_ap _ _ _ HFab) in *. set (H6 := pfstrx _ _ _ _ _ _ H5) in *. elim (ap_imp_less _ _ _ H6); clear H6 H5; intro. cut (Continuous_I (Min_leEq_Max a b) F). intro H4. 2: apply included_imp_Continuous with I; auto; apply included_interval; auto. set (incF := contin_imp_inc _ _ _ _ H4) in *. cut (Min a b [=] a). cut (Max a b [=] b); intros. 2: apply leEq_imp_Max_is_rht; apply less_leEq; auto. 2: apply leEq_imp_Min_is_lft; apply less_leEq; auto. set (Ha' := incF _ (compact_inc_lft _ _ (Min_leEq_Max a b))) in *. set (Hb' := incF _ (compact_inc_rht _ _ (Min_leEq_Max a b))) in *. cut (F _ Ha' [<] F _ Hb'). intro H7. apply Weak_IVT_ap_lft with (HFab := H7); auto. apply compact_wd' with (Hab := less_leEq _ _ _ HFab); algebra. astepl (F a Ha); astepr (F b Hb); auto. cut (Continuous_I (Min_leEq_Max b a) F). intro H4. 2: apply included_imp_Continuous with I; auto; apply included_interval; auto. set (incF := contin_imp_inc _ _ _ _ H4) in *. cut (Min a b [=] b). cut (Max a b [=] a); intros. 2: eapply eq_transitive_unfolded; [ apply Max_comm | apply leEq_imp_Max_is_rht; apply less_leEq; auto ]. 2: eapply eq_transitive_unfolded; [ apply Min_comm | apply leEq_imp_Min_is_lft; apply less_leEq; auto ]. set (Ha' := incF _ (compact_inc_lft _ _ (Min_leEq_Max b a))) in *. set (Hb' := incF _ (compact_inc_rht _ _ (Min_leEq_Max b a))) in *. cut (F _ Hb' [<] F _ Ha'). intro H7. elim (Weak_IVT_ap_rht _ _ _ _ H4 _ _ H7 _ H2 y); auto. intro x; intros. exists x; auto. apply compact_wd' with (Hab := Min_leEq_Max b a); [ apply Min_comm | apply Max_comm | auto ]. apply compact_wd' with (Hab := less_leEq _ _ _ HFab); algebra. apply pfwdef; astepl (Max a b); apply Max_comm. apply pfwdef; astepl (Min a b); apply Min_comm. apply less_wdl with (F a Ha). apply less_wdr with (F b Hb). auto. apply pfwdef; astepl (Min a b); apply Min_comm. apply pfwdef; astepl (Max a b); apply Max_comm. Qed.
imports: CoRN.ftc.WeakIVT CoRN.ftc.CalculusTheorems