tsum_ofReal_lt_top — Mathlib

English

If f: α → R is a real-valued summable sequence, then the ENNReal sum of real-to-ennreal images is finite: ∑' ENNReal.ofReal(f(i)) < ∞.

Русский

Пусть f: α → ℝ суммируема. Тогда сумма в окружении ENNReal от каждого f(i) конечна: ∑' ENNReal.ofReal(f(i)) < ∞.

LaTeX

$$$\text{Summable}(f) \implies \sum_i' \mathrm{ENNReal.ofReal}(f(i)) < \infty.$$$

Lean4

theorem tsum_ofReal_lt_top {f : α → ℝ} (hf : Summable f) : ∑' i, .ofReal (f i) < ∞ :=
  by
  unfold ENNReal.ofReal
  rw [lt_top_iff_ne_top, ENNReal.tsum_coe_ne_top_iff_summable]
  exact hf.toNNReal

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