proposition: Lemma ex_derive_filterdiff : forall (f : K -> V) (x : K), ex_derive f x <-> ex_filterdiff f (locally x).
proof: Proof. intros f x. split ; case => d Df. - eexists. exact Df. - exists (d one). split. apply is_linear_scal_l. simpl => t Ht. destruct Df as [Ld Df]. simpl in Df. apply domin_rw_r with (2 := Df t Ht). apply equiv_ext_loc. apply filter_forall => y. apply f_equal. rewrite -linear_scal //=. apply f_equal, sym_eq, mult_one_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv