integrable_finset_sum — Mathlib

English

Finite sums of integrable functions are integrable.

Русский

Конечные суммы интегрируемых функций интегрируемы.

LaTeX

$$$\\forall s: Finset\\, ι, \\forall f: ι\\to α\\to ε', \\Big( \\forall i∈s, Integrable (f i) μ \\Big) \\Rightarrow Integrable (\\sum_{i∈s} f i) μ$$$

Lean4

@[fun_prop]
theorem integrable_finset_sum {ι} (s : Finset ι) {f : ι → α → ε'} (hf : ∀ i ∈ s, Integrable (f i) μ) :
    Integrable (fun a => ∑ i ∈ s, f i a) μ := by simpa only [← Finset.sum_apply] using integrable_finset_sum' s hf

Похожие утверждения