English
For two linear trivializations e and e', and a base point b in the intersection, the coordinate-change map sends a vector y in F to the second component of the trivialization of (b, e.symm b y).
Русский
Для двух линейных тривиализаций e и e' и базовой точки b в пересечении координатное изменение отправляет вектор y в F в вторую компоненту тривиализации (b, e.symm b y).
LaTeX
$$$ coordChangeL R e e' b y = (e' ⟨b, e.symm b y⟩).2$.$$
Lean4
theorem symm_coordChangeL (e e' : Trivialization F (π F E)) [e.IsLinear R] [e'.IsLinear R] {b : B}
(hb : b ∈ e'.baseSet ∩ e.baseSet) : (e.coordChangeL R e' b).symm = e'.coordChangeL R e b :=
by
apply ContinuousLinearEquiv.toLinearEquiv_injective
rw [coe_coordChangeL' e' e hb, (coordChangeL R e e' b).toLinearEquiv_symm, coe_coordChangeL' e e' hb.symm,
LinearEquiv.trans_symm, LinearEquiv.symm_symm]
