proposition: Fact dopp (f : V -> W) x : differentiable f x -> continuous (- ('d f x : V -> W)) /\ (- f) \o shift x = cst (- f x) \- 'd f x +o_ (0 : V) id.
proof: Proof. move=> df; split; first by move=> ?; apply: continuousN. apply/eqaddoE; rewrite funeqE => y /=. by rewrite -[(- f) _]/(- (_ _)) diff_locallyx// !opprD oppox. 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