extChartAt_coe — Mathlib

English

The inverse of extChartAt at x equals the composition of chartAt at x inverse with I inverse; this clarifies how the inverse extended chart relates to the inverse standard chart and the model.

Русский

Обратная extChartAt в точке x равна композиции обратной chartAt с обратной моделью; это проясняет отношение обратной расширенной карты к обратной стандартной карте и модели.

LaTeX

$$$\\big(\\mathrm{extChartAt}(I,x)\\big)^{-1} = \\mathrm{chartAt}(H,x)^{-1} \\circ I^{-1}$$$

Lean4

theorem extChartAt_coe (x : M) : ⇑(extChartAt I x) = I ∘ chartAt H x :=
  rfl

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