localTriv_symm_apply — Mathlib

English

Whenever two local trivializations are co-supported at a base point, their coordinate-change maps agree on the shared fiber coordinate.

Русский

Если две локальные тривиализации имеют общий центр, переходы координат согласованы на общий фибер-координат.

LaTeX

$$$(Z.localTriv i).coordChangeL\,R\,(Z.localTriv j)\; b\; v = Z.coordChange\; i\; j\; b\; v$$$

Lean4

@[simp, mfld_simps]
theorem localTriv_symm_apply {b : B} (hb : b ∈ (Z.localTriv i).baseSet) (v : F) :
    (Z.localTriv i).symm b v = Z.coordChange i (Z.indexAt b) b v := by apply (Z.localTriv i).symm_apply hb v

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