extChartAt_target_union_compl_range_mem_nhds_of_mem

English

If [I.Boundaryless], then extChartAt I x . target is open.

Русский

Если [I.Boundaryless], то целевая область extChartAt I x открыта.

LaTeX

$$$ \\text{IsOpen}((\\mathrm{extChartAt} I x).\\mathrm{target})$$$

Lean4

theorem extChartAt_target_union_compl_range_mem_nhds_of_mem {y : E} {x : M} (hy : y ∈ (extChartAt I x).target) :
    (extChartAt I x).target ∪ (range I)ᶜ ∈ 𝓝 y :=
  by
  rw [← nhdsWithin_univ, ← union_compl_self (range I), nhdsWithin_union]
  exact Filter.union_mem_sup (extChartAt_target_mem_nhdsWithin_of_mem hy) self_mem_nhdsWithin

Похожие утверждения