map_extChartAt_nhdsWithin' — Mathlib

English

For x, y with y in the target, the symmetric chart extChartAt I x .symm is continuous at y.

Русский

Для x, y при условии y ∈ target, симметричная карта extChartAt I x .symm непрерывна в y.

LaTeX

$$$ y \\in (extChartAt I x).target \\Rightarrow \\text{ContinuousAt}((extChartAt I x).symm, y)$$$

Lean4

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

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