iteratedFDerivWithin_congr_set' — Mathlib

English

If nhds x equivalence on s and t, then iteratedFDerivWithin 𝕜 n f s x equals iteratedFDerivWithin 𝕜 n f t x for all n.

Русский

Если окрестность x эквивалентна между s и t, то производная порядка n совпадает для всех n.

LaTeX

$$$\forall h: (nhds x).EventuallyEq s t,\forall n, (iteratedFDerivWithin 𝕜 n f s x) = (iteratedFDerivWithin 𝕜 n f t x)$$$

Lean4

/-- If two sets coincide in a punctured neighborhood of `x`,
then the corresponding iterated derivatives are equal.

Note that we also allow to puncture the neighborhood of `x` at `y`.
If `y ≠ x`, then this is a no-op. -/
theorem iteratedFDerivWithin_congr_set' {y} (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) (n : ℕ) :
    iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x :=
  (iteratedFDerivWithin_eventually_congr_set' y h n).self_of_nhds

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