English
If a map is C^n on a set s in a manifold, then it is C^n at any point of s in the sense of ContMDiffAt.
Русский
Если отображение C^n на множестве s в многообразии, то оно является C^n в точке x ∈ s в смысле ContMDiffAt.
LaTeX
$$$ ContMDiffOn I I' n f s \Rightarrow ContMDiffAt I I' n f x \text{ for } x ∈ s $$$
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 contMDiffAt_iff_contMDiffAt_nhds [IsManifold I n M] [IsManifold I' n M'] (hn : n ≠ ∞) :
ContMDiffAt I I' n f x ↔ ∀ᶠ x' in 𝓝 x, ContMDiffAt I I' n f x' :=
by
refine ⟨?_, fun h => h.self_of_nhds⟩
rw [contMDiffAt_iff_contMDiffOn_nhds hn]
rintro ⟨u, hu, h⟩
refine (eventually_mem_nhds_iff.mpr hu).mono fun x' hx' => ?_
exact (h x' <| mem_of_mem_nhds hx').contMDiffAt hx'
