English
For two trivializations e and e', the map x ↦ e.coordChange e' (f x) (g x) is differentiable at x assuming differentiability of f and g in the appropriate models.
Русский
Для двух тривиализаций е и e', отображение x ↦ e.coordChange e' (f x) (g x) дифференцируемо в x при условии дифференцируемости f и g в соответствующих моделях.
LaTeX
$$$\displaystyle MDifferentiableAt IM IB f x \land MDifferentiableAt IM 𝓘(𝕜, F) g x \Rightarrow MDifferentiableAt IM 𝓘(𝕜, F) (\lambda y. e.coordChange e' (f y) (g y)) x.$$$
Lean4
theorem mdifferentiableAt_add_section (hs : MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) x₀)
(ht : MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (t x)) x₀) :
MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x ((s + t) x)) x₀ :=
by
rw [← mdifferentiableWithinAt_univ] at hs ht ⊢
apply mdifferentiableWithinAt_add_section hs ht
