map_extChartAt_symm_nhdsWithin — Mathlib

English

The symmetric chart maps nhdsWithin back to nhds within s: map (extChartAt I x).symm (nhdsWithin ((extChartAt I x).toFun x) (intersection with s)) = nhdsWithin x s.

Русский

Симметричная карта ExtChartAt возвращает nhdsWithin обратно в nhdsWithin s: аналогичное равенство для nhdsWithin.

LaTeX

$$$ \\text{map}(extChartAt I x).symm(\\mathcal{N}_{s}(extChartAt I x x)) = \\mathcal{N}_{s}(x)$$$

Lean4

theorem map_extChartAt_symm_nhdsWithin (x : M) :
    map (extChartAt I x).symm (𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x x) = 𝓝[s] x :=
  map_extChartAt_symm_nhdsWithin' (mem_extChartAt_source x)

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