English
If IsManifold I n M and I' n M' hold, then ContMDiffAt is equivalent to ContMDiffWithinAt which, in turn, is equivalent to ContMDiffOn near the point.
Русский
Если существуют условия IsManifold I n M и IsManifold I' n M', то ContMDiffAt эквивалентно ContMDiffWithinAt, которое эквивалентно ContMDiffOn в окрестности точки.
LaTeX
$$$ ContMDiffAt I I' n f x \iff ContMDiffWithinAt I I' n f Set.univ x \iff ContMDiffOn I I' n f Set.univ $$$
Lean4
/-- If a function is `C^m` within a set at a point, for some finite `m`, then it is `C^m` within
this set on a neighborhood of the basepoint. -/
theorem contMDiffOn [IsManifold I n M] [IsManifold I' n M'] (hm : m ≤ n) (h' : m = ∞ → n = ω)
(h : ContMDiffWithinAt I I' n f s x) : ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContMDiffOn I I' m f u :=
by
let ⟨_u, uo, xu, h⟩ := h.contMDiffOn' hm h'
exact ⟨_, inter_mem_nhdsWithin _ (uo.mem_nhds xu), inter_subset_left, h⟩
