localTriv_continuousLinearMapAt — Mathlib

English

If b lies in baseSet of i, then the continuous linear map of the trivialization at b equals coordChange between the i and indexAt b.

Русский

Если b принадлежит базовому множеству i, то непрерывное линейное отображение локальной тривиализации в b равно coordChange между i и indexAt(b).

LaTeX

$$$(Z.localTriv i).continuousLinearMapAt\; R\; b = Z.coordChange (Z.indexAt b) i b$$$

Lean4

@[simp, mfld_simps]
theorem localTriv_continuousLinearMapAt {b : B} (hb : b ∈ (Z.localTriv i).baseSet) :
    (Z.localTriv i).continuousLinearMapAt R b = Z.coordChange (Z.indexAt b) i b :=
  by
  ext1 v
  rw [(Z.localTriv i).continuousLinearMapAt_apply R, (Z.localTriv i).coe_linearMapAt_of_mem]
  exacts [rfl, hb]

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