iteratedFDerivWithin_congr_set — Mathlib

English

If nhdsWithin near x punctured at y yields equivalence of sets s and t, then iterated derivatives coincide for all orders at x.

Русский

Если nhdsWithin поблизости x с вырезом y эквивалентны множествам s и t, то производные совпадают для всех порядков в x.

LaTeX

$$$\forall y, (nhdsWithin x (HasCompl.singleton y)).EventuallyEq s t \Rightarrow \forall n, Eq (iteratedFDerivWithin 𝕜 n f s x) (iteratedFDerivWithin 𝕜 n f t x)$$$

Lean4

theorem iteratedFDerivWithin_congr_set (h : s =ᶠ[𝓝 x] t) (n : ℕ) :
    iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x :=
  (iteratedFDerivWithin_eventually_congr_set h n).self_of_nhds

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