continuousAt_extChartAt_symm — Mathlib

English

For any x, the map extChartAt I x .symm is continuous at any y in the target.

Русский

Для любого x карта extChartAt I x .symm непрерывна в любой точке y внутри target.

LaTeX

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

Lean4

theorem continuousAt_extChartAt_symm (x : M) : ContinuousAt (extChartAt I x).symm ((extChartAt I x) x) :=
  continuousAt_extChartAt_symm' (mem_extChartAt_source x)

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