iteratedDeriv_eq — Mathlib

English

If two functions are equal near x in the nhds sense, their nth iterated derivatives at x are equal.

Русский

Если две функции равны в окрестности точки x в смысле nhds, их n-я повторная производная в x равны.

LaTeX

$$$\\operatorname{iteratedDeriv}_n f x = \\operatorname{iteratedDeriv}_n g x$ if \\ f =ᶠ_{𝓝 x} g$$$

Lean4

theorem iteratedDeriv_eq (n : ℕ) {f g : 𝕜 → F} {x : 𝕜} (hfg : f =ᶠ[𝓝 x] g) :
    iteratedDeriv n f x = iteratedDeriv n g x :=
  by
  simp only [← iteratedDerivWithin_univ, iteratedDerivWithin_eq_iteratedFDerivWithin]
  rw [(hfg.filter_mono nhdsWithin_le_nhds).iteratedFDerivWithin_eq hfg.eq_of_nhds n]

Похожие утверждения