English
The target of extChartAt I x is contained in the closure of the interior of the target.
Русский
Target ExtChartAt I x содержится в замыкании внутренности целевой области.
LaTeX
$$$ (extChartAt I x).target \\subseteq \\overline{\\operatorname{int}( (extChartAt I x).target )}$$$
Lean4
theorem extChartAt_target_subset_closure_interior {x : M} :
(extChartAt I x).target ⊆ closure (interior (extChartAt I x).target) :=
by
intro y hy
rw [mem_closure_iff_nhds]
intro t ht
have A : t ∩ ((extChartAt I x).target ∪ (range I)ᶜ) ∈ 𝓝 y :=
inter_mem ht (extChartAt_target_union_compl_range_mem_nhds_of_mem hy)
have B : y ∈ closure (interior (range I)) := by
apply I.range_subset_closure_interior (extChartAt_target_subset_range x hy)
obtain ⟨z, ⟨tz, h'z⟩, hz⟩ : (t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∩ interior (range I)).Nonempty :=
mem_closure_iff_nhds.1 B _ A
refine ⟨z, ⟨tz, ?_⟩⟩
have h''z : z ∈ (extChartAt I x).target := by simpa [interior_subset hz] using h'z
exact (extChartAt_target_eventuallyEq_of_mem h''z).symm.mem_interior hz
