sSup_add

Mathlib.Data.ENNReal.Operations

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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