tsum_right — Mathlib

English

If a commutes with every term f(i), it commutes with the infinite sum: a commutes with ∑ f(i).

Русский

Если a коммутирует со всеми членами f(i), тогда a коммутирует с бесконечной суммой ∑ f(i).

LaTeX

$$$\forall i,\ Commute a (f(i)) \Rightarrow Commute a \ (\sum' i, f(i))$$$

Lean4

theorem tsum_right (a) (h : ∀ i, Commute a (f i)) : Commute a (∑'[L] i, f i) := by
  classical
  by_cases hf : Summable f L
  · exact (hf.tsum_mul_left a).symm.trans ((tsum_congr h).trans (hf.tsum_mul_right a))
  · exact (tsum_eq_zero_of_not_summable hf).symm ▸ Commute.zero_right _

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