summable

Mathlib.Topology.Instances.ENNReal.Lemmas

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

English

A function f: α → ENNReal is summable if there exists a HasSum for it.

Русский

Функция f: α → ENNReal суммируема, если существует представление HasSum.

LaTeX

$$∀ f, Summable f$$

Lean4

@[simp]
protected theorem summable : Summable f :=
  ⟨_, ENNReal.hasSum⟩

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

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

Разделы

Аффилиация

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