iteratedFDerivWithin_eq — Mathlib

English

If two functions agree on a punctured neighborhood of x outside y, then their iterated derivatives at x are equal for all orders when evaluated at x.

Русский

Если две функции совпадают в просветке вокруг x за пределами y, то их повторные производные в x совпадают для всех порядков.

LaTeX

$$$\forall n, \ iteratedFDerivWithin 𝕜 n f s x = \ iteratedFDerivWithin 𝕜 n f t x$$$

Lean4

/-- If two functions coincide in a neighborhood of `x` within a set `s` and at `x`, then their
iterated differentials within this set at `x` coincide. -/
theorem iteratedFDerivWithin_eq (h : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) (n : ℕ) :
    iteratedFDerivWithin 𝕜 n f₁ s x = iteratedFDerivWithin 𝕜 n f s x :=
  have : f₁ =ᶠ[𝓝[insert x s] x] f := by simpa [EventuallyEq, hx]
  (this.iteratedFDerivWithin' (subset_insert _ _) n).self_of_nhdsWithin (mem_insert _ _)

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