proposition: Lemma Weak_IVT_ap_lft : forall Ha Hb (HFab : F a Ha [<] F b Hb) e, [0] [<] e -> forall z, Compact (less_leEq _ _ _ HFab) z -> {x : IR | Compact Hab x | forall Hx, AbsIR (F x Hx[-]z) [<=] e}.
proof: Proof. intros Ha Hb HFab e H z H0. cut (a [<] b). intro Hab'. set (G := FAbs (F{-}[-C-]z)) in *. assert (H1 : Continuous_I Hab G). unfold G in |- *; Contin. set (m := glb_funct _ _ _ _ H1) in *. elim (glb_is_glb _ _ _ _ H1). fold m in |- *; intros. cut (forall x : IR, Compact Hab x -> forall Hx, m [<=] AbsIR (F x Hx[-]z)); [ clear a0; intro a0 | intros ]. elim (less_cotransitive_unfolded _ _ _ H m); intros. elim H0; clear H0; intros H0 H0'. cut (F a Ha[-]z [<=] [--]m); intros. cut (m [<=] F b Hb[-]z); intros. exfalso. elim (contin_prop _ _ _ _ contF m a1); intros d H4 H5. set (incF := contin_imp_inc _ _ _ _ contF) in *. set (f := fun i Hi => F (compact_part _ _ Hab' d H4 i Hi) (incF _ (compact_part_hyp _ _ Hab Hab' d H4 i Hi)) [-]z) in *. set (n := compact_nat a b d H4) in *. cut (forall i Hi, f i Hi [<=] [0]). intros. apply (less_irreflexive_unfolded _ (F b Hb[-]z)). eapply less_leEq_trans. 2: apply H3. apply leEq_less_trans with ZeroR. 2: auto. apply leEq_wdl with (f _ (le_n n)); auto. unfold f, compact_part, n in |- *; simpl in |- *. apply cg_minus_wd; [ apply pfwdef; rational | algebra ]. simple induction i. intros; unfold f, compact_part in |- *. apply leEq_wdl with (F a Ha[-]z). apply leEq_transitive with ( [--]m); auto. astepr ( [--]ZeroR); apply less_leEq; apply inv_resp_less; auto. apply cg_minus_wd; [apply pfwdef | idtac]; rational. intros i' Hrec HSi'. astepr (m[-]m). apply shift_leEq_minus'. cut (i' <= n); [ intro Hi' | auto with arith ]. apply leEq_transitive with ( [--] (f _ Hi') [+]f _ HSi'). apply plus_resp_leEq. cut ({m [<=] f _ Hi'} + {f _ Hi' [<=] [--]m}). intro; inversion_clear H6. exfalso. apply (less_irreflexive_unfolded _ m). apply leEq_less_trans with ZeroR. eapply leEq_transitive; [ apply H7 | apply (Hrec Hi') ]. auto. astepl ( [--][--]m); apply inv_resp_leEq; auto. apply leEq_distr_AbsIR. assumption. unfold f in |- *; apply a0; apply compact_part_hyp. rstepl (f _ HSi'[-]f _ Hi'). eapply leEq_transitive. apply leEq_AbsIR. unfold f in |- *; simpl in |- *. apply leEq_wdl with (AbsIR (F _ (incF _ (compact_part_hyp _ _ Hab Hab' d H4 _ HSi')) [-] F _ (incF _ (compact_part_hyp _ _ Hab Hab' d H4 _ Hi')))). apply H5; try apply compact_part_hyp. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. apply compact_leEq. apply less_leEq; apply compact_less. apply AbsIR_wd; rational. eapply leEq_wdr. 2: apply AbsIR_eq_x. apply a0; apply compact_inc_rht. apply shift_leEq_minus; astepl z; auto. astepl ( [--][--] (F a Ha[-]z)); apply inv_resp_leEq. eapply leEq_wdr. 2: apply AbsIR_eq_inv_x. apply a0; apply compact_inc_lft. apply shift_minus_leEq; astepr z; auto. elim (b0 (e[-]m)); intros. elim p; clear p b0; intros y Hy. elim Hy; intros. elim b0; clear b0; intros H2 H3. exists y; auto. intro. apply leEq_wdl with (G y H2). apply less_leEq. apply plus_cancel_less with ( [--]m). eapply less_wdl. apply q. unfold cg_minus in |- *; algebra. unfold G in |- *. apply eq_transitive_unfolded with (AbsIR (Part _ _ (ProjIR1 H2))). apply FAbs_char. apply AbsIR_wd; simpl in |- *; algebra. apply shift_less_minus; astepl m; auto. apply a0. exists x. split. auto. repeat split; auto. intro; unfold G in |- *. apply eq_transitive_unfolded with (AbsIR (Part _ _ (ProjIR1 Hy))). apply FAbs_char. apply AbsIR_wd; simpl in |- *; algebra. set (H1 := less_imp_ap _ _ _ HFab) in *. set (H2 := pfstrx _ _ _ _ _ _ H1) in *. elim (ap_imp_less _ _ _ H2); intro. auto. exfalso. apply (less_irreflexive_unfolded _ a). apply leEq_less_trans with b; auto. Qed.
imports: CoRN.ftc.Continuity