English
If s and t coincide locally around a point y in a specified sense, then MDifferentiableWithinAt agrees on s and t at x.
Русский
Если s и t совпадают локально вокруг точки y в заданном смысле, то MDifferentiableWithinAt совпадает на s и t в точке x.
LaTeX
$$$$MDifferentiableWithinAt I I' f s x \\iff MDifferentiableWithinAt I I' f t x \\text{ when } s =^\\!\\[\\mathcal{N}(\\{ y \\}^c)\\] t$$$$
Lean4
/-- If two sets coincide locally around `x`, except maybe at a point `y`, then their
preimage under `extChartAt x` coincide locally, except maybe at `extChartAt I x x`. -/
theorem preimage_extChartAt_eventuallyEq_compl_singleton (y : M) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) :
((extChartAt I x).symm ⁻¹' s ∩ range I : Set E) =ᶠ[𝓝[{extChartAt I x x}ᶜ] (extChartAt I x x)]
((extChartAt I x).symm ⁻¹' t ∩ range I : Set E) :=
by
have : T1Space M := I.t1Space M
obtain ⟨u, u_mem, hu⟩ : ∃ u ∈ 𝓝 x, u ∩ { x }ᶜ ⊆ {y | (y ∈ s) = (y ∈ t)} :=
mem_nhdsWithin_iff_exists_mem_nhds_inter.1 (nhdsWithin_compl_singleton_le x y h)
rw [← extChartAt_to_inv (I := I) x] at u_mem
have B : (extChartAt I x).target ∪ (range I)ᶜ ∈ 𝓝 (extChartAt I x x) :=
by
rw [← nhdsWithin_univ, ← union_compl_self (range I), nhdsWithin_union]
apply Filter.union_mem_sup (extChartAt_target_mem_nhdsWithin x) self_mem_nhdsWithin
apply
mem_nhdsWithin_iff_exists_mem_nhds_inter.2
⟨_, Filter.inter_mem ((continuousAt_extChartAt_symm x).preimage_mem_nhds u_mem) B, ?_⟩
rintro z ⟨hz, h'z⟩
simp only [eq_iff_iff, mem_setOf_eq]
change z ∈ (extChartAt I x).symm ⁻¹' s ∩ range I ↔ z ∈ (extChartAt I x).symm ⁻¹' t ∩ range I
by_cases hIz : z ∈ range I
· simp [-extChartAt, hIz] at hz ⊢
rw [← eq_iff_iff]
apply hu ⟨hz.1, ?_⟩
simp only [mem_compl_iff, mem_singleton_iff, ne_comm, ne_eq] at h'z ⊢
rw [(extChartAt I x).eq_symm_apply (by simp) hz.2]
exact Ne.symm h'z
· simp [hIz]
