iteratedDeriv_sub — Mathlib

English

If two functions are EventuallyEq close to each other at x, then their nth iterated derivatives at x are equal.

Русский

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

LaTeX

$$$\\text{Filter.EventuallyEq.iteratedDeriv}_n f x = \\text{Filter.EventuallyEq.iteratedDeriv}_n g x$$$

Lean4

theorem iteratedDeriv_sub (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
    iteratedDeriv n (f - g) x = iteratedDeriv n f x - iteratedDeriv n g x := by
  simpa only [iteratedDerivWithin_univ] using iteratedDerivWithin_sub (Set.mem_univ _) uniqueDiffOn_univ hf hg

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