isOpen_extChartAt_target — Mathlib

English

If y ∈ (extChartAt I x).target, then (extChartAt I x).target ∪ (range I)ᶜ ∈ 𝓝 y.

Русский

Если y ∈ целевой области, то объединение целевой области с дополнением к диапазону принадлежит 𝓝 y.

LaTeX

$$$ (extChartAt I x).target \\cup (range I)^{c} \\in 𝓝 y$$$

Lean4

/-- If we're boundaryless, `extChartAt` has open target -/
theorem isOpen_extChartAt_target [I.Boundaryless] (x : M) : IsOpen (extChartAt I x).target :=
  by
  simp_rw [extChartAt_target, I.range_eq_univ, inter_univ]
  exact (OpenPartialHomeomorph.open_target _).preimage I.continuous_symm

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