English
Let E be a C^n vector bundle over a manifold B modeled on F, with two C^n trivializations e and e'. The fiberwise coordinate change between these trivializations is a C^n map on the overlap of their domains, i.e. on e.baseSet ∩ e'.baseSet.
Русский
Пусть E — C^n векторное расслоение над многообразием B, моделируемое по F, с двумя тривиализациями e и e'. Координатный переход между этими тривиализациями по форме тензора является C^n отображением на пересечении областей определения, то есть на e.baseSet ∩ e'.baseSet.
LaTeX
$$$\\displaystyle \\text{Пусть }E\\text{ — }C^n\\text{ векторное расслоение над }B\\text{ моделируемое по }F.\\\\n\\text{Пусть }e,e'\\text{ — две }C^n\\text{ тривиализации }E.\\text{ Тогда переход между тривиализациями}\\;e.coordChange\,e'\\text{ является }C^n\\text{ на пересечении базовых множеств }e.baseSet\\cap e'.baseSet.$$$
Lean4
protected theorem coordChange (hf : ContMDiffOn IM IB n f s) (hg : ContMDiffOn IM 𝓘(𝕜, F) n g s)
(he : MapsTo f s e.baseSet) (he' : MapsTo f s e'.baseSet) :
ContMDiffOn IM 𝓘(𝕜, F) n (fun y ↦ e.coordChange e' (f y) (g y)) s := fun x hx ↦
(hf x hx).coordChange (hg x hx) (he hx) (he' hx)
