sum_comp_equiv — Mathlib

English

If e is an equivalence between index sets, then summing over i is the same as summing over e(i).

Русский

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

LaTeX

$$$ \text{sum } (μ \circ e) = \text{sum } μ $$$

Lean4

@[simp]
theorem sum_comp_equiv {ι ι' : Type*} (e : ι' ≃ ι) (m : ι → Measure α) : sum (m ∘ e) = sum m :=
  by
  ext s hs
  simpa [hs, sum_apply] using e.tsum_eq (fun n ↦ m n s)

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