English
Differentiability of a section in the total space is equivalent to differentiability of its base-projection and its fiber-coordinate under the trivialization, 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 mdifferentiableWithinAt_add_section
(hs : MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) u x₀)
(ht : MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (t x)) u x₀) :
MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x ((s + t) x)) u x₀ :=
by
rw [mdifferentiableWithinAt_section] at hs ht ⊢
set e := trivializationAt F E x₀
refine (hs.add ht).congr_of_eventuallyEq ?_ ?_
· apply eventually_of_mem (U := e.baseSet)
· exact mem_nhdsWithin_of_mem_nhds <| (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F E x₀)
· exact fun x hx ↦ (e.linear 𝕜 hx).1 ..
· exact (e.linear 𝕜 (FiberBundle.mem_baseSet_trivializationAt' x₀)).1 ..
