English
If f is MDifferentiableWithinAt on s, then it remains MDifferentiableWithinAt on insert y s for any y.
Русский
Если f дифференцируема внутри s, то она сохраняет это свойство при добавлении точки y.
LaTeX
$$$ (h : MDifferentiableWithinAt I I' f s x) \Rightarrow MDifferentiableWithinAt I I' f (insert y s) x $$$
Lean4
theorem hasMFDerivWithinAt_insert {y : M} :
HasMFDerivWithinAt I I' f (insert y s) x f' ↔ HasMFDerivWithinAt I I' f s x f' :=
by
have : T1Space M := I.t1Space M
refine ⟨fun h => h.mono <| subset_insert y s, fun hf ↦ ?_⟩
rcases eq_or_ne x y with rfl | h
· rw [HasMFDerivWithinAt] at hf ⊢
refine ⟨hf.1.insert, ?_⟩
have : (extChartAt I x).target ∈ 𝓝[(extChartAt I x).symm ⁻¹' insert x s ∩ range I] (extChartAt I x) x :=
nhdsWithin_mono _ inter_subset_right (extChartAt_target_mem_nhdsWithin x)
rw [← hasFDerivWithinAt_inter' this]
apply hf.2.insert.mono
rintro z ⟨⟨hz, h2z⟩, h'z⟩
simp only [mem_inter_iff, mem_preimage, mem_insert_iff, mem_range] at hz h2z ⊢
rcases hz with xz | h'z
· left
have : x ∈ (extChartAt I x).source := mem_extChartAt_source x
exact (((extChartAt I x).eq_symm_apply this h'z).1 xz.symm).symm
· exact Or.inr ⟨h'z, h2z⟩
· apply hf.mono_of_mem_nhdsWithin ?_
simp_rw [nhdsWithin_insert_of_ne h, self_mem_nhdsWithin]
