extChartAt_prod — Mathlib

English

The extended chart on a composition of charts is the composition of the corresponding charts, i.e., extChartAt I x equals the transitive composition of charts.

Русский

Расширенная карта на композицию карт равна композиции соответствующих карт.

LaTeX

$$$extChartAt I x = (chartAt H' x) \toPartialEquiv \circ extChartAt I (chartAt H' x x)$$$

Lean4

theorem extChartAt_prod (x : M × M') : extChartAt (I.prod I') x = (extChartAt I x.1).prod (extChartAt I' x.2) :=
  by
  simp only [mfld_simps]
  rw [PartialEquiv.prod_trans]

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