continuousAt_extChartAt_symm'' — Mathlib

English

If y lies in the target, then the inverse chart (extChartAt I x).symm is continuous at 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 continuousAt_extChartAt_symm'' {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
    ContinuousAt (extChartAt I x).symm y :=
  continuousAt_extend_symm' _ h

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