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