fact: CoInductive differentiable_def (f : V -> W) (x : filter_on V) (phF : phantom (set (set V)) x) : Prop := DifferentiableDef of (continuous ('d f x) /\ f = cst (f (lim x)) + 'd f x \o center (lim x) +o_x (center (lim x))).
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms