extChartAt_to_inv — Mathlib

English

The chart extChartAt I x is invertible on its image; applying the inverse to the image returns x.

Русский

Карта extChartAt I x взаимно однозначна на образе; обращение возвращает x.

LaTeX

$$$ (\\mathrm{extChartAt}\\ I\\ x).\\mathrm{symm}((\\mathrm{extChartAt}\\ I\\ x)\\ x) = x$$$

Lean4

theorem extChartAt_to_inv (x : M) : (extChartAt I x).symm ((extChartAt I x) x) = x :=
  (extChartAt I x).left_inv (mem_extChartAt_source x)

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