proposition: Lemma diffE (F : filter_on V) (f : V -> W) : differentiable f F -> forall x, f x = f (lim F) + 'd f F (x - lim F) +o_(x \near F) (x - lim F).
proof: Proof. by move=> /diffP []. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms