lintegral_finset_sum — Mathlib

English

For a Finset s and functions f_b with each f_b measurable, the lintegral of the sum equals the sum of lintegrals.

Русский

Для конечного множества s и функций f_b, каждая из которых измерима, линеграл суммы равен сумме линегралов.

LaTeX

$$$\forall s : Finset \beta, \forall f : \beta \to (\alpha \to \mathbb{R}_{\ge 0}^{\infty}),\; (\forall b \in s, Measurable (f b)) \Rightarrow ∫^- a, \sum_{b \in s} f b a \partial\mu = \sum_{b \in s} ∫^- a, f b a \partial\mu$$$

Lean4

theorem lintegral_finset_sum (s : Finset β) {f : β → α → ℝ≥0∞} (hf : ∀ b ∈ s, Measurable (f b)) :
    ∫⁻ a, ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ a, f b a ∂μ :=
  lintegral_finset_sum' s fun b hb => (hf b hb).aemeasurable

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