proposition: Lemma diff_eqO (V' W' : normedModType R) (x : filter_on V') (f : V' -> W') : differentiable f x -> ('d f x : V' -> W') =O_ (0 : V') id.
proof: Proof. by move=> /diff_continuous /linear_eqO; apply. 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