proposition: Lemma filterdiff_continuous_aux {F} {FF : Filter F} (f : U -> V) : ex_filterdiff f F -> forall x, is_filter_lim F x -> filterlim f F (locally (f x)).
proof: Proof. intros [l [Hl Df]] x Hx. specialize (Df x Hx). apply filterlim_locally_ball_norm => eps. specialize (Df (mkposreal _ Rlt_0_1)) ; simpl in Df. destruct (linear_norm _ Hl) as [M Hm]. assert (F (fun y => norm (minus (f y) (f x)) <= (M + 1) * norm (minus y x))). move: Df ; apply filter_imp => y Hy. rewrite Rmult_1_l in Hy. apply Rle_trans with (1 := norm_triangle_inv _ _) in Hy. apply Rabs_le_between' in Hy. eapply Rle_trans. by apply Hy. apply Rle_minus_r ; ring_simplify. by apply Hm. move: H => {} Df. assert (Hm': 0 < M + 1). apply Rplus_le_lt_0_compat. apply Rlt_le, Hm. exact Rlt_0_1. assert (0 < eps / (M+1)). apply Rdiv_lt_0_compat with (2 := Hm'). apply cond_pos. specialize (Hx _ (locally_ball_norm x (mkposreal _ H))). generalize (filter_and _ _ Hx Df) => /=. apply filter_imp => y [Hy Hy'] {Hx Df}. apply Rle_lt_trans with (1 := Hy'). evar_last. now apply Rmult_lt_compat_l with (2 := Hy). field. now apply Rgt_not_eq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv