sum_nonneg

Mathlib.Topology.PartitionOfUnity

URI: https://scilib.ai/kg/mathlib#PartitionOfUnity.sum_nonneg

English

The sum over i of f_i(x) is nonnegative for any x.

Русский

Сумма по i от f_i(x) неотрицательна для любого x.

LaTeX

$$$\forall x,\ 0 \le \sum_{i}^{\text{fin}} f_i(x)$$$

Lean4

theorem sum_nonneg (x : X) : 0 ≤ ∑ᶠ i, f i x :=
  finsum_nonneg fun i => f.nonneg i x

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

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

Разделы

Аффилиация

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