English
If a scalar function f and a section s are differentiable within a set u at x0, then the product f · s is differentiable within u at x0.
Русский
Если скалярная функция f и секция s дифференциируемы в окрестности x0 внутри множества u, то произведение f · s дифференцируемо там же.
LaTeX
$$$ MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (\x => TotalSpace.mk' F x (f x \cdot s x)) u x_0$ given differentiability of f and s within u at x0$$
Lean4
theorem smul_section (hf : MDifferentiableWithinAt I 𝓘(𝕜) f u x₀)
(hs : MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) u x₀) :
MDifferentiableWithinAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (f x • s x)) u x₀ :=
by
rw [mdifferentiableWithinAt_section] at hs ⊢
set e := trivializationAt F E x₀
refine (hf.smul hs).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).2 ..
· apply (e.linear 𝕜 (FiberBundle.mem_baseSet_trivializationAt' x₀)).2
