map_extChartAt_nhds — Mathlib

English

The pushforward of the neighborhood of x by extChartAt I x equals the nhds within range I at extChartAt I x x.

Русский

Образ окрестности x под extChartAt I x равен \\nhds внутри range I в extChartAt I x x.

LaTeX

$$$ map (\\mathrm{extChartAt} I x) (\\mathcal{N} x) = \\mathcal{N}_{\\mathrm{range} I}(\\mathrm{extChartAt} I x x)$$$

Lean4

theorem map_extChartAt_nhds (x : M) : map (extChartAt I x) (𝓝 x) = 𝓝[range I] extChartAt I x x :=
  map_extChartAt_nhds' <| mem_extChartAt_source x

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