le_one

Mathlib.Topology.PartitionOfUnity

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

English

The full (finite) sum is bounded above by 1 for every x.

Русский

Полная конечная сумма не превышает единицу для каждого x.

LaTeX

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

Lean4

theorem le_one (i : ι) (x : X) : f i x ≤ 1 :=
  (single_le_finsum i (f.locallyFinite.point_finite x) fun j => f.nonneg j x).trans (f.sum_le_one x)

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

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

Разделы

Аффилиация

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