extChartAt_preimage_mem_nhds_of_mem_nhdsWithin

English

Let x ∈ M and suppose x' lies in the source of the chart extChartAt I x. If s is a neighborhood of extChartAt I x x' within the chart's range, then the preimage of s under extChartAt I x is a neighborhood of x'.

Русский

Пусть x ∈ M и пусть x' принадлежит источнику extChartAt I x. Если s является окрестностью extChartAt I x x' внутри диапазона карты, то ее предобраз под extChartAt I x является окрестностью x'.

LaTeX

$$$x' ∈ (\mathrm{extChartAt} I x).\text{source} \quad\Rightarrow\quad (\mathrm{extChartAt} I x)^{-1} s \in 𝓝(x').$$$

Lean4

theorem extChartAt_preimage_mem_nhds_of_mem_nhdsWithin {s : Set E} {x x' : M} (hx : x' ∈ (extChartAt I x).source)
    (hs : s ∈ 𝓝[range I] (extChartAt I x x')) : (extChartAt I x) ⁻¹' s ∈ 𝓝 x' :=
  extend_preimage_mem_nhds_of_mem_nhdsWithin _ (by simpa using hx) hs

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