English
If two sets agree on nhds x, then their iterated derivatives at x agree for all n.
Русский
Если множества совпадают в окрестности x, их производные совпадают в x для всех n.
LaTeX
$$$\forall h: (nhds x).EventuallyEq s t,\forall n, (iteratedFDerivWithin 𝕜 n f s x) = (iteratedFDerivWithin 𝕜 n f t x)$$$
Lean4
/-- The iterated differential within a set `s` at a point `x` is not modified if one intersects
`s` with a neighborhood of `x` within `s`. -/
theorem iteratedFDerivWithin_inter' {n : ℕ} (hu : u ∈ 𝓝[s] x) :
iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x :=
iteratedFDerivWithin_congr_set (nhdsWithin_eq_iff_eventuallyEq.1 <| nhdsWithin_inter_of_mem' hu) _