iteratedFDerivWithin — Mathlib

English

If functions f and f1 are equal in a neighborhood of x within s, then their iterated derivatives within s at x coincide for all orders.

Русский

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

LaTeX

$$$\forall n, (nhdsWithin x s).EventuallyEq (iteratedFDerivWithin 𝕜 n f1 s) (iteratedFDerivWithin 𝕜 n f s)$$$

Lean4

protected theorem iteratedFDerivWithin (h : f₁ =ᶠ[𝓝[s] x] f) (n : ℕ) :
    iteratedFDerivWithin 𝕜 n f₁ s =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f s :=
  h.iteratedFDerivWithin' Subset.rfl n

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