English
For a VectorPrebundle a and any two pretrivializations e, e' in its atlas, there is a fiberwise linear map coordChange between them, depending on the base point b, i.e., a.coordChange e he e' he' is a map F →L[R] F.
Русский
Для VectorPrebundle a и любых двух предривиализаций e, e' из его атласа существует переход координат между ними, задающийся на каждом базовом точке b и являющийся линейным отображением по волокну: a.coordChange e he e' he' : F →L[R] F.
LaTeX
$$$\\\\forall e,e' \\\\in a.pretrivializationAtlas:\\\\ ∀ (hb : e \\\\ baseSet \\\\cap e' \\\\ baseSet) \\\\ ∀ b \\\\in B \\\\_\\, (a.coordChange e he e' he') b : F →L[R] F.$$$
Lean4
/-- A randomly chosen coordinate change on a `VectorPrebundle`, given by
the field `exists_coordChange`. -/
def coordChange (a : VectorPrebundle R F E) {e e' : Pretrivialization F (π F E)} (he : e ∈ a.pretrivializationAtlas)
(he' : e' ∈ a.pretrivializationAtlas) (b : B) : F →L[R] F :=
Classical.choose (a.exists_coordChange e he e' he') b
