English
Given two linear trivializations, there is a canonical coordinate change that glues them on the intersection, matching the base and fiber coordinates.
Русский
Дано две линейные тривиализации, существует каноническое изменение координат, склеивающее их на пересечении и согласующее базовые и волокновые координаты.
LaTeX
$$$ e e' : Trivialization F (\pi F E) \Rightarrow coordChangeL R e e' b is defined on b \in e.baseSet \cap e'.baseSet;$$$
Lean4
theorem coe_coordChangeL' (e e' : Trivialization F (π F E)) [e.IsLinear R] [e'.IsLinear R] {b : B}
(hb : b ∈ e.baseSet ∩ e'.baseSet) :
(coordChangeL R e e' b).toLinearEquiv = (e.linearEquivAt R b hb.1).symm.trans (e'.linearEquivAt R b hb.2) :=
LinearEquiv.coe_injective (coe_coordChangeL _ _ hb)
