proposition: Lemma derivable1_diffP f x : derivable f x 1 <-> differentiable f x.
proof: Proof. split=> dfx. by apply/diff_locallyP; rewrite deriv1E //; split; [apply: scalel_continuous|apply: der1]. apply/derivable_nbhsP/eqaddoE. have -> : (fun h => (f \o shift x) h%:A) = f \o shift x. by rewrite funeqE=> ?; rewrite [_%:A]mulr1. by have /diff_locally := dfx; rewrite diff1E // derive1E =>->. 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