English
For a VectorPrebundle a and charts e, e' with b in their intersection, the equality (b, a.coordChange e he e' he' b v) = e' ⟨b, e.symm b v⟩ holds and matches the previous expansion.
Русский
Для VectorPrebundle a и диаграмм 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
/-- Natural identification of `VectorPrebundle` as a `FiberPrebundle`. -/
def toFiberPrebundle (a : VectorPrebundle R F E) : FiberPrebundle F E :=
{ a with
continuous_trivChange := fun e he e' he' ↦
by
have : ContinuousOn (fun x : B × F ↦ a.coordChange he' he x.1 x.2) ((e'.baseSet ∩ e.baseSet) ×ˢ univ) :=
isBoundedBilinearMap_apply.continuous.comp_continuousOn
((a.continuousOn_coordChange he' he).prodMap continuousOn_id)
rw [e.target_inter_preimage_symm_source_eq e', inter_comm]
refine (continuousOn_fst.prodMk this).congr ?_
rintro ⟨b, f⟩ ⟨hb, -⟩
dsimp only [Function.comp_def, Prod.map]
rw [a.mk_coordChange _ _ hb, e'.mk_symm hb.1] }
