English
If x lies in the closure of the interior of s, then extChartAt I x maps x into the closure of the interior of s after taking the appropriate preimage under the symmetry.
Русский
Если x принадлежит замыканиюInterior s, тогда extChartAt I x x лежит в замыкании Interior (extChartAt I x).symm⁻¹' s ∩ (extChartAt I x).target.
LaTeX
$$$ x_0\\in \\overline{\\operatorname{interior}s} \\;\; \\rightarrow \\; extChartAt I x_0 x \\in \\overline{\\operatorname{interior} (extChartAt I x_0)^{-1}' s \\cap (extChartAt I x_0).target}$$$
Lean4
theorem extChartAt_mem_closure_interior {x₀ x : M} (hx : x ∈ closure (interior s))
(h'x : x ∈ (extChartAt I x₀).source) :
extChartAt I x₀ x ∈ closure (interior ((extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target)) :=
by
simp_rw [mem_closure_iff, interior_inter, ← inter_assoc]
intro o o_open ho
obtain ⟨y, ⟨yo, hy⟩, ys⟩ : ((extChartAt I x₀) ⁻¹' o ∩ (extChartAt I x₀).source ∩ interior s).Nonempty :=
by
have : (extChartAt I x₀) ⁻¹' o ∈ 𝓝 x := by
apply (continuousAt_extChartAt' h'x).preimage_mem_nhds (o_open.mem_nhds ho)
refine (mem_closure_iff_nhds.1 hx) _ (inter_mem this ?_)
apply (isOpen_extChartAt_source x₀).mem_nhds h'x
have A : interior (↑(extChartAt I x₀).symm ⁻¹' s) ∈ 𝓝 (extChartAt I x₀ y) :=
by
simp only [interior_mem_nhds]
apply (continuousAt_extChartAt_symm' hy).preimage_mem_nhds
simp only [hy, PartialEquiv.left_inv]
exact mem_interior_iff_mem_nhds.mp ys
have B : (extChartAt I x₀) y ∈ closure (interior (extChartAt I x₀).target) :=
by
apply extChartAt_target_subset_closure_interior (x := x₀)
exact (extChartAt I x₀).map_source hy
exact mem_closure_iff_nhds.1 B _ (inter_mem (o_open.mem_nhds yo) A)
