add_sSup

Mathlib.Data.ENNReal.Operations

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

English

For any nonempty set s, a + sSup s = ⨆ b∈s, a + b.

Русский

Для непустого множества s: a + sSup s = ⨆_{b∈s} (a + b).

LaTeX

$$$a + sSup s = \\displaystyle \\big\\sup_{b\\in s} (a + b\\big)$$$

Lean4

theorem add_sSup (hs : s.Nonempty) : a + sSup s = ⨆ b ∈ s, a + b := by rw [sSup_eq_iSup, add_biSup hs]

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

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

Разделы

Аффилиация

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