iSup_add

Mathlib.Data.ENNReal.Operations

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

English

The supremum of a family plus a fixed amount equals the supremum of the pointwise sums: (sup_i f_i) + a = sup_i (f_i + a).

Русский

Супремум семейства плюс фиксированная константа равна супремуму по i от (f_i + a).

LaTeX

$$$\\sup_i f_i + a = \\sup_i (f_i + a)$$$

Lean4

theorem iSup_add [Nonempty ι] (f : ι → ℝ≥0∞) : (⨆ i, f i) + a = ⨆ i, f i + a := by simp [add_comm, add_iSup]

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

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

Разделы

Аффилиация

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