English
If a function is differentiable in a neighborhood in a set and the order is finite, then near the point x, differentiability of the same order persists on a neighborhood within the set.
Русский
Если функция дифференцируема в окрестности множества и конечен порядок, то вближайшей окрестности точки x дифференцируемость такого порядка сохраняется внутри множества.
LaTeX
$$$\forall h : ContDiffWithinAt 𝕜 n f s x, n \neq \infty \Rightarrow \forall y$ близко к x внутри s, $ContDiffWithinAt 𝕜 n f s y$.$$
Lean4
protected theorem eventually (h : ContDiffWithinAt 𝕜 n f s x) (hn : n ≠ ∞) :
∀ᶠ y in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 n f s y :=
by
rcases h.contDiffOn le_rfl (by simp [hn]) with ⟨u, hu, _, hd⟩
have : ∀ᶠ y : E in 𝓝[insert x s] x, u ∈ 𝓝[insert x s] y ∧ y ∈ u := (eventually_eventually_nhdsWithin.2 hu).and hu
refine this.mono fun y hy => (hd y hy.2).mono_of_mem_nhdsWithin ?_
exact nhdsWithin_mono y (subset_insert _ _) hy.1
