sum_comm — Mathlib

English

If e is a bijection between index sets, then summing μ over i is same as summing μ over e(i): sum μ = sum (μ ∘ e).

Русский

Если e — эквивалентность между индексами, то сумма по i равна сумме по e(i): sum μ = sum (μ ∘ e).

LaTeX

$$$ \sum_{i} μ_i = \sum_{i'} μ_{e(i')} $$$

Lean4

theorem sum_comm {ι' : Type*} (μ : ι → ι' → Measure α) : (sum fun n => sum (μ n)) = sum fun m => sum fun n => μ n m :=
  by
  ext1 s hs
  simp_rw [sum_apply _ hs]
  rw [ENNReal.tsum_comm]

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