sum_add_sum_compl — Mathlib

English

Sum of sums distributes over addition: sum μ + sum ν = sum (n ↦ μ_n + ν_n).

Русский

Сумма сумм распределяется по сложению: sum μ + sum ν = sum (n ↦ μ_n + ν_n).

LaTeX

$$$ \sum μ + \sum ν = \sum_n (μ_n + ν_n) $$$

Lean4

theorem sum_add_sum_compl (s : Set ι) (μ : ι → Measure α) : ((sum fun i : s => μ i) + sum fun i : ↥sᶜ => μ i) = sum μ :=
  by
  ext1 t ht
  simp only [add_apply, sum_apply _ ht]
  exact ENNReal.summable.tsum_add_tsum_compl (f := fun i => μ i t) ENNReal.summable

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