English
Let {t_i} be a locally finite family of sections of a vector bundle E → B, and suppose each map x ↦ TotalSpace.mk' F x (t_i x) is differentiable in the coordinate sense. Then the infinite sum, taken with finite support at each point, defines a differentiable section x ↦ TotalSpace.mk' F x (∑ᶠ_i t_i x) of the same bundle (in the sense of the chosen differentiability structure).
Русский
Пусть имеется локально конечнаяFamily секций т_i в векторном расслоении E → B, и пусть для каждого i отображение x ↦ TotalSpace.mk' F x (t_i x) дифференцируемо в заданной координатной системе. Тогда сумма Σᶠ_i t_i x задаёт дифференцируемую секцию данного расслоения.
LaTeX
$$$\\text{LocallyFinite }\\{i \\mapsto t_i\\} \\;\wedge\\; \\forall i,\\; MDiffI(I)(Iprod\\; 𝓘(\\mathbb{k},F))(x \\mapsto \\text{TotalSpace.mk}' F x (t_i x))\\n\\Rightarrow\\; MDiffI(Iprod\\; 𝓘(\\mathbb{k},F))(x \\mapsto \\text{TotalSpace.mk}' F x (\\sum^\\mathrm{fin}_i t_i x)).$$$
Lean4
theorem finsum_section_of_locallyFinite (ht : LocallyFinite fun i ↦ {x : B | t i x ≠ 0})
(ht' : ∀ i, MDifferentiable I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (t i x))) :
MDifferentiable I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (∑ᶠ i, t i x)) := fun x ↦
.finsum_section_of_locallyFinite ht fun i ↦ ht' i x
