collapse_nonneg

Mathlib.Combinatorics.SetFamily.FourFunctions

URI: https://scilib.ai/kg/mathlib#collapse_nonneg

English

If all f_i are nonnegative, then collapse 𝒜 a f is nonnegative; in particular 0 ≤ collapse 𝒜 a f.

Русский

Если все f_i неотрицательны, то collapse 𝒜 a f неотрицателен; следовательно 0 ≤ collapse 𝒜 a f.

LaTeX

$$0 ≤ collapse 𝒜 a f$$

Lean4

theorem collapse_nonneg (hf : 0 ≤ f) : 0 ≤ collapse 𝒜 a f := fun _s ↦ sum_nonneg fun _t _ ↦ hf _

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

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

Разделы

Аффилиация

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