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]