English
If b lies in the intersection of the base sets, the coordinate-change map at b applied to v equals the second component of the trivialization e' evaluated at (b, e.symm b v).
Русский
Если b лежит в пересечении базовых множеств, переход координат в точке b, применённый к v, равен второй компоненте тривиализации e' в выражении (b, e.symm b v).
LaTeX
$$$$ b \\\\in e.baseSet \\\\cap e'.baseSet \\\\Rightarrow a.coordChange e he e' he' b v = (e' \\\\langle b, e.symm b v \\\\rangle).2. $$$$
Lean4
theorem mk_coordChange (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) : (b, a.coordChange he he' b v) = e' ⟨b, e.symm b v⟩ :=
by
ext
· rw [e.mk_symm hb.1 v, e'.coe_fst', e.proj_symm_apply' hb.1]
rw [e.proj_symm_apply' hb.1]
exact hb.2
· exact a.coordChange_apply he he' hb v
