proposition: Lemma derivable_nbhsxP (f : V -> W) a v : derivable f a v <-> forall h, f (a + h *: v) = f a + h *: 'D_v f a +o_(h \near (nbhs (0 :R))) h.
proof: Proof. split; first exact: derivable_nbhsx. move=> df; apply/derivable_nbhsP; apply/eqaddoE; rewrite funeqE => h. by rewrite /= addrC df. 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