localTriv_symm_apply — Mathlib

English

The forward map of the i-th local trivialization is compatible with the right-hand side by applying coordChange with indexAt p.1.

Русский

Применение локальной тривиализации iigo согласовано с правой частью через coordChange с indexAt p.1.

LaTeX

$$$\\text{localTriv_symm_apply}(i,p) \\;:=$\\; (Z.localTriv i)^{\\mathrm{symm}}.toFun' p = (p.1, Z.coordChange i (Z.indexAt p.1) p.1 p.2)$$$

Lean4

@[simp, mfld_simps]
theorem localTriv_symm_apply (p : B × F) :
    (Z.localTriv i).toOpenPartialHomeomorph.symm p = ⟨p.1, Z.coordChange i (Z.indexAt p.1) p.1 p.2⟩ :=
  rfl

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