English
If two sets agree puncturedly near x, then their iterated derivatives coincide at x for all orders.
Русский
Если две множества совпадают в окрестности x за исключением точки, то их итеративные производные совпадают в x на любом порядке.
LaTeX
$$$\forall y, (s =ᶠ[𝓝[{y}]^c x] t) \Rightarrow \forall n, (iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x).$$$
Lean4
/-- If two functions coincide on a set `s`, then their iterated differentials within this set
coincide. See also `Filter.EventuallyEq.iteratedFDerivWithin_eq` and
`Filter.EventuallyEq.iteratedFDerivWithin`. -/
theorem iteratedFDerivWithin_congr (hs : EqOn f₁ f s) (hx : x ∈ s) (n : ℕ) :
iteratedFDerivWithin 𝕜 n f₁ s x = iteratedFDerivWithin 𝕜 n f s x :=
(hs.eventuallyEq.filter_mono inf_le_right).iteratedFDerivWithin_eq (hs hx) _
