English
For two trivializations e and e' that overlap, the coordinate-change maps between their local trivializations vary continuously with the base point. In other words, the map b ↦ coordChangeL(R, e, e', b) is continuous on the overlap e.baseSet ∩ e'.baseSet.
Русский
Для двух тривиализаций e и e', которые имеют общую область, переход между локальными тривиализациями изменяется непрерывно по базовой точке. То есть отображение b ↦ coordChangeL(R, e, e', b) непрерывно на пересечении базовых множеств.
LaTeX
$$$b \mapsto \operatorname{coordChangeL}(R, e, e', b)\in \mathrm{End}_R(F)$ непрерывно на $e.baseSet \cap e'.baseSet$$$
Lean4
theorem continuousOn_coordChange [VectorBundle R F E] (e e' : Trivialization F (π F E)) [MemTrivializationAtlas e]
[MemTrivializationAtlas e'] :
ContinuousOn (fun b => Trivialization.coordChangeL R e e' b : B → F →L[R] F) (e.baseSet ∩ e'.baseSet) :=
VectorBundle.continuousOn_coordChange' e e'
