trivializationAt_symmL — Mathlib

English

There is a linear relation between the symmetric linear map L of the trivialization and coordChange.

Русский

Существует линейное отношение между симметрической линейной картой L тривиализации и coordChange.

LaTeX

$$$trivializationAt\_symmL\; R\; (Z) = Z.coordChange (Z.indexAt b₀) (Z.indexAt b) b$$$

Lean4

@[simp, mfld_simps]
theorem trivializationAt_symmL {b₀ b : B} (hb : b ∈ (trivializationAt F Z.Fiber b₀).baseSet) :
    (trivializationAt F Z.Fiber b₀).symmL R b = Z.coordChange (Z.indexAt b₀) (Z.indexAt b) b :=
  Z.localTriv_symmL hb

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