English
If m ≤ n and the germ is witnessed by an open neighborhood, then there exists a neighborhood where ContMDiffOn holds for insert x s.
Русский
Если m ≤ n и существут окрестности, на которых ContMDiffOn выполняется для insert x s, то существует такое же окрестность.
LaTeX
$$$ ContMDiffOn I I' m f s \exists U, x ∈ U ∧ ContMDiffOn I I' m f (insert x s ∩ U) $$$
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 an open set around 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, IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I' m f (insert x s ∩ u) :=
by
have : IsManifold I m M := .of_le hm
have : IsManifold I' m M' := .of_le hm
match m with
| (m : ℕ) |
ω =>
rcases (contMDiffWithinAt_iff_contMDiffOn_nhds (by simp)).1 (h.of_le hm) with ⟨t, ht, h't⟩
rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩
rw [inter_comm] at hu
exact ⟨u, u_open, xu, h't.mono hu⟩
| ∞ =>
rcases (contMDiffWithinAt_iff_contMDiffOn_nhds (by simp [h'])).1 h with ⟨t, ht, h't⟩
rcases mem_nhdsWithin.1 ht with ⟨u, u_open, xu, hu⟩
rw [inter_comm] at hu
exact ⟨u, u_open, xu, (h't.mono hu).of_le hm⟩
