English
Insertion of the base point into the domain does not affect the C^n within-At property at the base point.
Русский
Добавление базовой точки в область определения не влияет на свойство C^n внутри-At в базовой точке.
LaTeX
$$$ ContMDiffWithinAt I I' n f (insert x s) x \iff ContMDiffWithinAt I I' n f s x $$$
Lean4
/-- A function is `C^n` within a set at a point, for `n : ℕ` or `n = ω`,
if and only if it is `C^n` on a neighborhood of this point. -/
theorem contMDiffWithinAt_iff_contMDiffOn_nhds [IsManifold I n M] [IsManifold I' n M'] (hn : n ≠ ∞) :
ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u := by
-- WLOG, `x ∈ s`, otherwise we add `x` to `s`
wlog hxs : x ∈ s generalizing s
· rw [← contMDiffWithinAt_insert_self, this (mem_insert _ _), insert_idem]
rw [insert_eq_of_mem hxs]
-- The `←` implication is trivial
refine
⟨fun h ↦ ?_, fun ⟨u, hmem, hu⟩ ↦ (hu _ (mem_of_mem_nhdsWithin hxs hmem)).mono_of_mem_nhdsWithin hmem⟩
-- The property is true in charts. Let `v` be a good neighborhood in the chart where the function
-- is `Cⁿ`.
rcases (contMDiffWithinAt_iff'.1 h).2.contDiffOn le_rfl (by simp [hn]) with ⟨v, hmem, hsub, hv⟩
have hxs' :
extChartAt I x x ∈ (extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) :=
⟨(extChartAt I x).map_source (mem_extChartAt_source _), by rwa [extChartAt_to_inv], by rw [extChartAt_to_inv];
apply mem_extChartAt_source⟩
rw [insert_eq_of_mem hxs'] at hmem hsub
refine ⟨(extChartAt I x).symm '' v, ?_, ?_⟩
· rw [← map_extChartAt_symm_nhdsWithin (I := I),
h.1.nhdsWithin_extChartAt_symm_preimage_inter_range (I := I) (I' := I')]
exact image_mem_map hmem
· have hv₁ : (extChartAt I x).symm '' v ⊆ (extChartAt I x).source :=
image_subset_iff.2 fun y hy ↦ (extChartAt I x).map_target (hsub hy).1
have hv₂ : MapsTo f ((extChartAt I x).symm '' v) (extChartAt I' (f x)).source :=
by
rintro _ ⟨y, hy, rfl⟩
exact (hsub hy).2.2
rwa [contMDiffOn_iff_of_subset_source' hv₁ hv₂, PartialEquiv.image_symm_image_of_subset_target]
exact hsub.trans inter_subset_left
