map_extChartAt_nhds_of_boundaryless

English

If [I.Boundaryless], the pushforward of nhds x is just nhds of extChartAt I x x.

Русский

Если [I.Boundaryless], то образ nhds x через extChartAt I x совпадает с nhds (extChartAt I x x).

LaTeX

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

Lean4

theorem map_extChartAt_nhds_of_boundaryless [I.Boundaryless] (x : M) :
    map (extChartAt I x) (𝓝 x) = 𝓝 (extChartAt I x x) :=
  by
  rw [extChartAt]
  exact map_extend_nhds_of_boundaryless (chartAt H x) (mem_chart_source H x)

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