proposition: Lemma differentiableP (R : numDomainType) (V W : normedModType R) (f : V -> W) x : differentiable f x -> is_diff x f ('d f x).
proof: Proof. by move=> ?; apply: DiffDef. 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