localTriv_coordChange_eq — Mathlib

English

The coordinate-change map between two local trivializations equals the core's coordinate change, when applied to a point and fiber element.

Русский

Переход координат между двумя локальными тривиализациями равен переходу ядра при применении к точке и элементу волокна.

LaTeX

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

Lean4

@[simp, mfld_simps]
theorem localTriv_coordChange_eq {b : B} (hb : b ∈ (Z.localTriv i).baseSet ∧ b ∈ (Z.localTriv j).baseSet) (v : F) :
    (Z.localTriv i).coordChangeL R (Z.localTriv j) b v = Z.coordChange i j b v :=
  by
  rw [Trivialization.coordChangeL_apply', localTriv_symm_fst, localTriv_apply, coordChange_comp]
  exacts [⟨⟨hb.1, Z.mem_baseSet_at b⟩, hb.2⟩, hb]

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