English
For a C^n vector bundle with a trivialization pair e and e', the coordinate change map between them is C^n in the fiber coordinates over the base where both trivializations are defined.
Русский
Переход coordChange между тривиализациями гладок класса C^n в базовом пространстве B.
LaTeX
$$$$\\text{Пусть }E\\text{ — }C^n\\text{ векторное расслоение над }B,\\;e,e'\\text{ тривиализации. }\\\\coordChange\\!:\\!e.baseSet\\cap e'.baseSet\\to GL(F)^{B}\\text{ гладкость по }n.$$$$
Lean4
protected theorem coordChange (hf : ContMDiff IM IB n f) (hg : ContMDiff IM 𝓘(𝕜, F) n g) (he : ∀ x, f x ∈ e.baseSet)
(he' : ∀ x, f x ∈ e'.baseSet) : ContMDiff IM 𝓘(𝕜, F) n (fun y ↦ e.coordChange e' (f y) (g y)) := fun x ↦
(hf x).coordChange (hg x) (he x) (he' x)
