add_iInf

Mathlib.Data.ENNReal.Operations

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

English

Adding a fixed ENNReal a to an iInf commutes: a + iInf f = iInf (a + f i).

Русский

Прибавление константы к iInf сохраняется: a + iInf f = iInf (a + f i).

LaTeX

$$$ a + \mathrm{iInf}\ f = \mathrm{iInf}\ (\lambda i. a + f(i)) $$$

Lean4

theorem add_iInf {a : ℝ≥0∞} : a + iInf f = ⨅ b, a + f b := by rw [add_comm, iInf_add]; simp [add_comm]

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

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

Разделы

Аффилиация

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