proposition: Lemma Continuous_imp_comm_Lim : forall F x e, [0] [<] e -> Continuous (clcr (Lim x[-]e) (Lim x[+]e)) F -> forall Hx Hxn H, F (Lim x) Hx [=] Lim (Build_CauchySeq IR (fun n => F (x n) (Hxn n)) H).
proof: Proof. intros F x e H H0 Hx Hxn H1. set (a := Lim x) in *. set (I := clcr (a[-]e) (a[+]e)) in *. cut (compact_ I). intro H2. 2: simpl in |- *. 2: apply less_leEq; apply less_transitive_unfolded with a. 2: apply shift_minus_less; apply shift_less_plus'. 2: astepl ZeroR; auto. 2: apply shift_less_plus'. 2: astepl ZeroR; auto. apply Limits_unique. simpl in |- *. intros eps H3. set (H2' := H2) in *. cut (Continuous_I (a:=Lend H2) (b:=Rend H2) H2' F). intro H4. 2: apply Int_Continuous; auto. elim (contin_prop _ _ _ _ H4 _ H3); intros d H5 H6. elim (Cauchy_complete x (Min d e)). 2: apply less_Min; auto. intros N HN. exists N; intros. fold a in HN. apply AbsIR_imp_AbsSmall. elim (HN m H7); intros. apply H6. split; simpl in |- *. unfold cg_minus in |- *; apply shift_plus_leEq'. eapply leEq_transitive. 2: apply H8. apply inv_resp_leEq; apply Min_leEq_rht. apply shift_leEq_plus'. eapply leEq_transitive. apply H9. apply Min_leEq_rht. split; simpl in |- *. apply shift_minus_leEq; apply shift_leEq_plus'. astepl ZeroR; apply less_leEq; auto. apply shift_leEq_plus'; astepl ZeroR. apply less_leEq; auto. apply AbsSmall_imp_AbsIR. apply AbsSmall_leEq_trans with (Min d e). apply Min_leEq_lft. auto. Qed.
imports: CoRN.ftc.Rolle CoRN.tactics.DiffTactics3