extChartAt_target_mem_nhdsWithin_of_mem

English

If y ∈ (extChartAt I x).target, then (extChartAt I x).target ∈ 𝓝[range I] extChartAt I x y.

Русский

Если y ∈ целевой области, то целевая область ∈ 𝓝[range I] extChartAt I x y.

LaTeX

$$$ (extChartAt I x).target ∈ 𝓝[range I] extChartAt I x y$$$

Lean4

theorem extChartAt_target_mem_nhdsWithin_of_mem {x : M} {y : E} (hy : y ∈ (extChartAt I x).target) :
    (extChartAt I x).target ∈ 𝓝[range I] y :=
  by
  rw [← (extChartAt I x).right_inv hy]
  apply extChartAt_target_mem_nhdsWithin'
  exact (extChartAt I x).map_target hy

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