English
If a function f is differentiable on a set s, then the map b ↦ e.coordChangeL 𝕜 e' (f b) is differentiable on s as a function into linear endomorphisms of F whenever f(b) lands in the base sets of both trivializations.
Русский
Если функция f дифференцируема на множество s, то отображение b ↦ e.coordChangeL 𝕜 e' (f(b)) дифференцируемо на s как отображение в линейные эндоморфизмы пространства F при условии, что f(b) попадает в базы обеих тривиализаций.
LaTeX
$$$\displaystyle MDifferentiableOn\!\, IM \mathcal{I}(\mathbb{K}, F \to_L[\mathbb{K}] F) (\lambda b. (e.coordChangeL 𝕜 e' (f b) : F \to_L[\mathbb{K}] F)) \, s \ x.$$$$
Lean4
protected theorem coordChangeL (hf : MDifferentiableOn IM IB f s) (he : MapsTo f s e.baseSet)
(he' : MapsTo f s e'.baseSet) :
MDifferentiableOn IM 𝓘(𝕜, F →L[𝕜] F) (fun y ↦ (e.coordChangeL 𝕜 e' (f y) : F →L[𝕜] F)) s := fun x hx ↦
(hf x hx).coordChangeL (he hx) (he' hx)
