summable_toNNReal_of_tsum_ne_top — Mathlib

English

If ∑' i, f(i) ≠ ∞, then Summable (toNNReal ∘ f).

Русский

Если сумма не бесконечна, то композиция toNNReal с f квадратируется суммируемой.

LaTeX

$$$\text{HasSum } f? or\; \text{Summable } (\mathrm{toNNReal} \circ f)$$$

Lean4

theorem summable_toNNReal_of_tsum_ne_top {α : Type*} {f : α → ℝ≥0∞} (hf : ∑' i, f i ≠ ∞) :
    Summable (ENNReal.toNNReal ∘ f) := by
  simpa only [← tsum_coe_ne_top_iff_summable, toNNReal_apply_of_tsum_ne_top hf] using hf

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