English
C^n at a point implies C^n on a neighborhood functionally, with a germ-compatible extension.
Русский
C^n в точке влечет C^n на окрестности через локальное расширение согласованного germs.
LaTeX
$$$ ContMDiffAt I I' n f x \Rightarrow \exists U \ni x, ContMDiffOn I I' n f U $$$
Lean4
/-- Note: This does not hold for `n = ∞`. `f` being `C^∞` at `x` means that for every `n`, `f` is
`C^n` on some neighborhood of `x`, but this neighborhood can depend on `n`. -/
theorem contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin [IsManifold I n M] [IsManifold I' n M'] (hn : n ≠ ∞) :
ContMDiffWithinAt I I' n f s x ↔ ∀ᶠ x' in 𝓝[insert x s] x, ContMDiffWithinAt I I' n f s x' :=
by
refine ⟨?_, fun h ↦ mem_of_mem_nhdsWithin (mem_insert x s) h⟩
rw [contMDiffWithinAt_iff_contMDiffOn_nhds hn]
rintro ⟨u, hu, h⟩
filter_upwards [hu, eventually_mem_nhdsWithin_iff.mpr hu] with x' h'x' hx'
apply (h x' h'x').mono_of_mem_nhdsWithin
exact nhdsWithin_mono _ (subset_insert x s) hx'
