proposition: Lemma diff_lin (V' W' : normedModType R) (f : {linear V' -> W'}) x : continuous f -> 'd f x = f :> (V' -> W').
proof: Proof. by move=> fcont; apply/diff_unique => //; apply: dlin. 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