summable_toReal

Mathlib.Topology.Instances.ENNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#ENNReal.summable_toReal

English

If the ENNReal sum ∑ f(x) is finite, then the sum of the real parts (toReal) is summable.

Русский

Если сумма ENNReal конечна, то сумма действительных частей (toReal) сходится.

LaTeX

$$$\\sum' x, (f x).toReal$ is summable if $\\sum' x, f x ≠ ∞$$$

Lean4

theorem summable_toReal {f : α → ℝ≥0∞} (hsum : ∑' x, f x ≠ ∞) : Summable fun x => (f x).toReal :=
  (hasSum_toReal hsum).summable

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

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

Разделы

Аффилиация

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