tsum_ofReal_ne_top

Mathlib.Topology.Instances.ENNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#Summable.tsum_ofReal_ne_top

English

If f: α → ℝ is summable, then ∑' i ENNReal.ofReal(f(i)) ≠ ∞.

Русский

Если f: α → ℝ суммируема, то сумма ENNReal.ofReal(f(i)) не бесконечна.

LaTeX

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

Lean4

theorem tsum_ofReal_ne_top {f : α → ℝ} (hf : Summable f) : ∑' i, .ofReal (f i) ≠ ∞ :=
  hf.tsum_ofReal_lt_top.ne

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru