hsum_equiv — Mathlib

English

The sum of a summable family is invariant under a bijection of the index set.

Русский

Сумма суммируемой семейства сохраняется при биекционной переиндексации множества индексов.

LaTeX

$$$ (Equiv\, e\, s).hsum = s.hsum $$$

Lean4

@[simp]
theorem hsum_equiv (e : α ≃ β) (s : SummableFamily Γ R α) : (Equiv e s).hsum = s.hsum :=
  by
  ext g
  simp only [coeff_hsum, Equiv_toFun]
  exact finsum_eq_of_bijective e.symm (Equiv.bijective e.symm) fun x => rfl

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