proposition: Lemma differentiable_continuous (x : V) (f : V -> W) : differentiable f x -> {for x, continuous f}.
proof: Proof. move=> /diff_locallyP [dfc]; rewrite -addrA. rewrite (littleo_bigO_eqo (cst (1 : R))); last first. by apply/eqOP; near=> k; rewrite /cst [`|1|]normr1 mulr1; near do by []. rewrite addfo; first by move=> /eqolim; rewrite cvg_comp_shift add0r. by apply/eqolim0P; apply: (cvg_trans (dfc 0)); rewrite linear0. Unshelve. all: by end_near. 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