English
Under a fixed trivialization, differentiability of a section into the total space is equivalent to the joint differentiability of its base-projection and its fiber coordinates at a point.
Русский
При фиксированной тривиализации дифференцируемость секции в полном пространстве эквивалентна совместной дифференцируемости её проекции на основание и координат волокна в точке.
LaTeX
$$$\displaystyle MDifferentiableWithinAt IM IB f s x \iff (MDifferentiableWithinAt IM IB (\lambda y. (f y).proj) s x \land MDifferentiableWithinAt IM 𝓘(𝕜, F) (\lambda y. (e (f y)).2) s x).$$$
Lean4
theorem mdifferentiableOn_neg_section (hs : MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) u) :
MDifferentiableOn I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (-s x)) u := fun x₀ hx₀ ↦
mdifferentiableWithinAt_neg_section (hs x₀ hx₀)
