sum_add — Mathlib

English

For Countable ι, Kernel.sum (n ↦ κ n + η n) = Kernel.sum κ + Kernel.sum η.

Русский

Для счётного ι сумма κ_n+η_n равна сумме κ_n плюс сумма η_n.

LaTeX

$$$[Countable \\\\iota] \\\\Rightarrow Kernel.sum (fun n => κ n + η n) = Kernel.sum κ + Kernel.sum η$$$

Lean4

theorem sum_add [Countable ι] (κ η : ι → Kernel α β) : (Kernel.sum fun n => κ n + η n) = Kernel.sum κ + Kernel.sum η :=
  by
  ext a s hs
  simp only [coe_add, Pi.add_apply, sum_apply, Measure.sum_apply _ hs, Pi.add_apply, Measure.coe_add,
    ENNReal.summable.tsum_add ENNReal.summable]

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