tsum_eq_iSup_sum — Mathlib

English

For any f: α → ENNReal, the total sum equals the supremum of finite partial sums: ∑' a, f a = ⨆ s : Finset α, ∑ a ∈ s, f a.

Русский

Для любой f: α → ENNReal сумма равна верхней границе конечных частичных сумм.

LaTeX

$$$\\sum' a, f(a) = \\bigl\\langle \\!\\!\\!\\!\\! \\sup_{s \\in Finset(α)} \\sum_{a \\in s} f(a) \\bigr\\rangle.$$$

Lean4

protected theorem tsum_eq_iSup_sum : ∑' a, f a = ⨆ s : Finset α, ∑ a ∈ s, f a :=
  ENNReal.hasSum.tsum_eq

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