biSup_add

Mathlib.Data.ENNReal.Operations

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

English

With nonempty s, (sup_{i∈s} f_i) + a = sup_{i∈s} (f_i + a).

Русский

Для непустого s: (sup_{i∈s} f_i) + a = sup_{i∈s} (f_i + a).

LaTeX

$$$\\bigl(\\sup_{i\\in s} f_i\\bigr) + a = \\sup_{i\\in s} (f_i + a)$$$

Lean4

theorem biSup_add {ι : Type*} {s : Set ι} (hs : s.Nonempty) (f : ι → ℝ≥0∞) : (⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a :=
  biSup_add' hs _

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

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

Разделы

Аффилиация

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