English
If a section f: M → TotalSpace F E is MDifferentiableWithinAt and the associated components are differentiable, then the section obtained by replacing the fiber by a different trivialization is MDifferentiableWithinAt after composing with the same base map.
Русский
Если секция f: M → TotalSpace F E дифференцируема внутри и соответствующие компоненты дифференцируемы, то секция, полученная заменой тривиализации, остаётся дифференцируемой после композиции с тем же базовым отображением.
LaTeX
$$$\text{If } hf : MDifferentiableWithinAt IM IB f s x,\; he' : f x ∈ e'.baseSet, \; he : f x ∈ e.baseSet,\; \text{then } MDifferentiableWithinAt IM 𝓘(\mathbb{K}, F) (\lambda y. e' (f y)) s x.$$$
Lean4
protected theorem coordChange (hf : MDifferentiable IM IB f) (hg : MDifferentiable IM 𝓘(𝕜, F) g)
(he : ∀ x, f x ∈ e.baseSet) (he' : ∀ x, f x ∈ e'.baseSet) :
MDifferentiable IM 𝓘(𝕜, F) (fun y ↦ e.coordChange e' (f y) (g y)) := fun x ↦
(hf x).coordChange (hg x) (he x) (he' x)
