English
Let hf be differentiability of a function f within a subset s relative to an IM-IB structure, and suppose f(x) lies in the base sets of two trivializations e and e'. Then the map y ↦ e.coordChangeL 𝕜 e' (f y) is differentiable within s at x with target model 𝓘(𝕜, F →L[𝕜] F).
Русский
Пусть hf задаёт дифференцируемость функции f внутри множества s относительно структуры IM-IB, и пусть f(x) лежит в базовых множествах тривиализаций e и e'. Тогда отображение y ↦ e.coordChangeL 𝕜 e' (f y) дифференцируемо внутри s в точке x, с целью 𝓘(𝕜, F →L[𝕜] F).
LaTeX
$$$\displaystyle \text{If } hf : MDifferentiableWithinAt IM IB f \, s \, x,\; he : f x \in e.baseSet,\; he' : f x \in e'.baseSet,\quad\ MDifferentiableWithinAt\!\; IM \, 𝓘(\mathbb{K}, F \to_L[\mathbb{K}] F)\; (\lambda y. (e.coordChangeL 𝕜 e' (f y) : F \to_L[\mathbb{K}] F)) \; s \; x.$$$
Lean4
protected theorem coordChangeL (hf : MDifferentiableWithinAt IM IB f s x) (he : f x ∈ e.baseSet)
(he' : f x ∈ e'.baseSet) :
MDifferentiableWithinAt IM 𝓘(𝕜, F →L[𝕜] F) (fun y ↦ (e.coordChangeL 𝕜 e' (f y) : F →L[𝕜] F)) s x :=
(mdifferentiableAt_coordChangeL he he').comp_mdifferentiableWithinAt _ hf
