coe_coordChange — Mathlib

English

Let Z be a vector bundle core. Then the coordinate change map arising from the fiber bundle core agrees with the coordinate change map of the core when evaluated at any index pair (i, j) and any base point b.

Русский

Пусть Z есть ядро векторного расслоения. Тогда переходы координат, получаемые из фибер-бандла ядра, совпадают с переходами координат ядра при произвольной паре индексов (i, j) и базовой точке b.

LaTeX

$$$Z.toFiberBundleCore.coordChange\; i\; j\; b = Z.coordChange\; i\; j\; b$$$

Lean4

@[simp, mfld_simps]
theorem coe_coordChange (i j : ι) : Z.toFiberBundleCore.coordChange i j b = Z.coordChange i j b :=
  rfl

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