continuousAt_extChartAt_symm' — Mathlib

English

The same assertion as above, but stated in a simplified form: (extChartAt I x).symm is continuous at any point in the source chart.

Русский

То же самое утверждение в упрощенной форме: симметричная карта extChartAt I x .symm непрерывна в любой точке в области определения графа.

LaTeX

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

Lean4

theorem continuousAt_extChartAt_symm' {x x' : M} (h : x' ∈ (extChartAt I x).source) :
    ContinuousAt (extChartAt I x).symm (extChartAt I x x') :=
  continuousAt_extChartAt_symm'' <| (extChartAt I x).map_source h

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