English
If a family of functions indexed by i is interval-integrable for each i, then the finitely supported or suitably summed function is interval-integrable.
Русский
Если для каждого индекса i функция интервально интегрируема, то функция их конечной суммирования/функций с конечной опорой также интервал-интегрируема.
LaTeX
$$$\forall i, \operatorname{IntervalIntegrable}(f_i,\mu,a,b) \Rightarrow \operatorname{IntervalIntegrable}(\operatorname{finsum}_{i} f_i,\mu,a,b)$$$
Lean4
theorem sum {ε} [TopologicalSpace ε] [ENormedAddCommMonoid ε] [ContinuousAdd ε] (s : Finset ι) {f : ι → ℝ → ε}
(h : ∀ i ∈ s, IntervalIntegrable (f i) μ a b) : IntervalIntegrable (∑ i ∈ s, f i) μ a b :=
⟨integrable_finset_sum' s fun i hi => (h i hi).1, integrable_finset_sum' s fun i hi => (h i hi).2⟩
