sum_le_one

Mathlib.Topology.PartitionOfUnity

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

English

For any x, the finsum of the f_i(x) is at most 1.

Русский

Для любого x сумма по i от f_i(x) по конечному смыслу не превышает единицу.

LaTeX

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

Lean4

theorem sum_le_one (x : X) : ∑ᶠ i, f i x ≤ 1 :=
  f.sum_le_one' x

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

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

Разделы

Аффилиация

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