map_extChartAt_nhdsWithin — Mathlib

English

If x and x' are such that x' lies in the source of extChartAt I x, then the symmetric map is continuous at extChartAt I x x'.

Русский

Если x' принадлежит источнику extChartAt I x, то симметричная карта непрерывна в extChartAt I x x'.

LaTeX

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

Lean4

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

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