English
Let a be a VectorPrebundle and e, e' two pretrivializations with b in their overlap. Then the pair (b, a.coordChange e he e' he' b v) equals the point in the second trivialization e' with coordinates (b, e.symm b v).
Русский
Пусть a — VectorPrebundle, и e, e' — две предтривиализации с общим b. Тогда пара (b, a.coordChange e he e' he' b v) совпадает с точкой в тривиализации e' с координатами (b, e.symm b v).
LaTeX
$$$$ (b, a.coordChange e he e' he' b v) = e' \\\\langle b, e.symm b v \\\\rangle. $$$$
Lean4
theorem coordChange_apply (a : VectorPrebundle R F E) {e e' : Pretrivialization F (π F E)}
(he : e ∈ a.pretrivializationAtlas) (he' : e' ∈ a.pretrivializationAtlas) {b : B} (hb : b ∈ e.baseSet ∩ e'.baseSet)
(v : F) : a.coordChange he he' b v = (e' ⟨b, e.symm b v⟩).2 :=
(Classical.choose_spec (a.exists_coordChange e he e' he')).2 b hb v
