extChartAt_coe_symm — Mathlib

English

The source of extChartAt equals the source of chartAt, confirming that extending preserves the original chart domain.

Русский

Область определения extChartAt равна области определения chartAt; расширение сохраняет исходную область карты.

LaTeX

$$$\\mathrm{source}(\\mathrm{extChartAt}(I,x)) = \\mathrm{source}(\\mathrm{chartAt}\\,H\\,x)$$$

Lean4

theorem extChartAt_coe_symm (x : M) : ⇑(extChartAt I x).symm = (chartAt H x).symm ∘ I.symm :=
  rfl

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