proposition: Lemma diff_locallyxP (x : V) (f : V -> W) : differentiable f x <-> continuous ('d f x) /\ forall h, f (h + x) = f x + 'd f x h +o_(h \near 0 : V) h.
proof: Proof. split=> [dxf|[dfc dxf]]. split => //; apply: eqaddoEx => h; have /diffE -> := dxf. rewrite lim_id // addrK; congr (_ + _); rewrite littleo_center0 /= addrK. by congr ('o); rewrite funeqE => k /=; rewrite addrK. apply/diffP; split=> //; apply: eqaddoEx; move=> y. rewrite lim_id // -[in LHS](subrK x y) dxf; congr (_ + _). rewrite -(comp_centerK x id) -[X in the_littleo _ _ _ X](comp_centerK x). by rewrite -[_ (y - x)]/((_ \o (center x)) y) -littleo_center0. 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