English
If a finite family of ContMDiffWithinAt sections t_i is given, their sum ∑ t_i is ContMDiffWithinAt.
Русский
Если имеется конечное число ContMDiffWithinAt секций t_i, их сумма ∑ t_i гладка внутри области.
LaTeX
$$ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (∑ i ∈ s, (t i x))) u x0$$
Lean4
theorem smul_section (hf : ContMDiffWithinAt I 𝓘(𝕜) n f u x₀)
(hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) u x₀) :
ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (f x • s x)) u x₀ :=
by
rw [contMDiffWithinAt_section] at hs ⊢
set e := trivializationAt F V 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 V x₀)
· intro x hx
apply (e.linear 𝕜 hx).2
· apply (e.linear 𝕜 (FiberBundle.mem_baseSet_trivializationAt' x₀)).2
