localTriv_symmL — Mathlib

English

There is a natural equality between localTrivAt and the i-indexed localTriv.

Русский

Существует естественное равенство между localTrivAt и локальной тривиализацией, индексированной i.

LaTeX

$$$Z.localTrivAt b = Z.localTriv (Z.indexAt b)$$$

Lean4

@[simp, mfld_simps]
theorem localTriv_symmL {b : B} (hb : b ∈ (Z.localTriv i).baseSet) :
    (Z.localTriv i).symmL R b = Z.coordChange i (Z.indexAt b) b :=
  by
  ext1 v
  rw [(Z.localTriv i).symmL_apply R, (Z.localTriv i).symm_apply]
  exacts [rfl, hb]

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