proposition: Lemma diff_locallyx (x : V) (f : V -> W) : differentiable f x -> forall h, f (h + x) = f x + 'd f x h +o_(h \near 0 : V) h.
proof: Proof. by move=> /diff_locallyxP []. 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