English
For a VectorPrebundle a and any two pretrivializations e, e' in its atlas, the coordinate-change map a.coordChange e he e' he' is continuous on the overlap e.baseSet ∩ e'.baseSet.
Русский
Для VectorPrebundle a и любых двух предтривиализаций e, e' из атласа переход координат a.coordChange e he e' he' непрерывен на пересечении их базовых множеств.
LaTeX
$$$\\\\forall a \\\\ (e,e') \\\\in a.pretrivializationAtlas:\\\\ ContinuousOn (a.coordChange e he e' he') (e.baseSet \\\\cap e'.baseSet). $$$$
Lean4
theorem continuousOn_coordChange (a : VectorPrebundle R F E) {e e' : Pretrivialization F (π F E)}
(he : e ∈ a.pretrivializationAtlas) (he' : e' ∈ a.pretrivializationAtlas) :
ContinuousOn (a.coordChange he he') (e.baseSet ∩ e'.baseSet) :=
(Classical.choose_spec (a.exists_coordChange e he e' he')).1
