extChartAt_source — Mathlib

English

The inverse of extChartAt equals the composition of the inverse of chartAt with the inverse of I, showing a clean relationship between the extended chart and the base chart.

Русский

Обратная extChartAt равна композиции обратной chartAt с обратной I; демонстрирует простую связь между расширенной и базовой картами.

LaTeX

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

Lean4

theorem extChartAt_source (x : M) : (extChartAt I x).source = (chartAt H x).source :=
  extend_source _

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