map_extChartAt_symm_nhdsWithin' — Mathlib

English

The image of the nhds within s under extChartAt I x equals the nhdsWithin of extChartAt I x x over the intersection with s.

Русский

Образ nhdsWithin s под extChartAt I x равен nhdsWithin по extChartAt I x x на пересечении с s.

LaTeX

$$$ \\forall x,y:\\; y\\in (extChartAt I x).source \\Rightarrow \\text{map}(extChartAt I x)(\\mathcal{N}[s]y) = \\mathcal{N}[extChartAt I x''( (extChartAt I x).source \\cap s)](extChartAt I x y)$$$

Lean4

theorem map_extChartAt_symm_nhdsWithin' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    map (extChartAt I x).symm (𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x y) = 𝓝[s] y :=
  map_extend_symm_nhdsWithin _ <| by rwa [← extChartAt_source I]

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