English
Let {t_i} be a locally finite family of sections of a vector bundle with fibers V_x over a manifold M. If each map x ↦ TotalSpace.mk' F x (t_i(x)) is C^k, then the section x ↦ TotalSpace.mk' F x (∑' i, t_i(x)) is C^k. Equivalently, the sum of a locally finite collection of C^k-sections is C^k.
Русский
Пусть {t_i} — локально конечная совокупность секций векторного расслоения над многообразием M, где каждой точке x соответствует in V_x. Если для каждой i отображение x ↦ TotalSpace.mk' F x (t_i(x)) является C^k, то сумма по i в смысле суммирования finsum: x ↦ TotalSpace.mk' F x (∑' i, t_i(x)) также является C^k. Эквивалентно: сумма локально конечной совокупности C^k- секций сохраняет гладкость.
LaTeX
$$$\operatorname{LocallyFinite}\,\bigl(i \mapsto \{x \in M \mid t_i(x) \neq 0\}\bigr) \land \bigl(\forall i,\ ContMDiff I (I.prod 𝓘(𝕜, F)) n (x \mapsto \mathrm{TotalSpace.mk'} F x (t_i(x)))\bigr) \Rightarrow \ ContMDiff I (I.prod 𝓘(𝕜, F)) n (x \mapsto \mathrm{TotalSpace.mk'} F x (\sum' i, t_i(x)))$$$
Lean4
/-- The sum of a locally finite collection of sections is `C^k` iff each section is. -/
theorem sum_section_of_locallyFinite (ht : LocallyFinite fun i ↦ {x : M | t i x ≠ 0})
(ht' : ∀ i, ContMDiff I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (t i x))) :
ContMDiff I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (∑' i, (t i x))) := fun x ↦
.sum_section_of_locallyFinite ht fun i ↦ ht' i x
