English
Let e and e' be two trivializations of a vector bundle over B with fiber F. If x lies in both base sets, then the coordinate-change map b ↦ e.coordChangeL 𝕜 e' b, viewed as a map into the space of linear endomorphisms of F, is differentiable at x.
Русский
Пусть e и e' — две тривиализации векторного расслоения над базой B с правым волокном F. Если x принадлежит обоим базовым множествам, то отображение b ↦ e.coordChangeL 𝕜 e' b, рассматриваемое как отображение в пространство линейных отображений F→F, дифференцируемо в точке x.
LaTeX
$$$\displaystyle \text{If } x \in e.baseSet \text{ and } x \in e'.baseSet,\quad MDifferentiableAt\!\; IB \, \mathcal{I}(\mathbb{K}, F \to_L[\mathbb{K}] F)\; (\lambda b: B. (e.coordChangeL \; 𝕜 \; e'\; b))\ x.$$$
Lean4
theorem mdifferentiableAt_coordChangeL {x : B} (h : x ∈ e.baseSet) (h' : x ∈ e'.baseSet) :
MDifferentiableAt IB 𝓘(𝕜, F →L[𝕜] F) (fun b : B ↦ (e.coordChangeL 𝕜 e' b : F →L[𝕜] F)) x :=
(contMDiffAt_coordChangeL h h').mdifferentiableAt le_rfl
