sum_lt_top

Mathlib.Data.ENNReal.BigOperators

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

English

A sum is finite if and only if each summand is finite.

Русский

Сумма конечна тогда и только тогда, когда каждый член суммы конечен.

LaTeX

$$$\sum_{x\in s} f(x) < \infty \;\Leftrightarrow\; \forall x \in s,\ f(x) < \infty$$$

Lean4

/-- A sum is finite iff all summands are finite. -/
@[simp]
theorem sum_lt_top : ∑ a ∈ s, f a < ∞ ↔ ∀ a ∈ s, f a < ∞ :=
  WithTop.sum_lt_top

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

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

Разделы

Аффилиация

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