map_extChartAt_nhds' — Mathlib

English

If y ∈ (extChartAt I x).source, then the image of nhds y under extChartAt I x equals nhds within range I at extChartAt I x y.

Русский

Если y ∈ source extChartAt I x, то образ nhds y через extChartAt I x равен nhdsWithin (range I) на extChartAt I x y.

LaTeX

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

Lean4

theorem map_extChartAt_nhds' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    map (extChartAt I x) (𝓝 y) = 𝓝[range I] extChartAt I x y :=
  map_extend_nhds _ <| by rwa [← extChartAt_source I]

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