add_sInf

Mathlib.Data.ENNReal.Operations

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

English

For any set s, adding a fixed a to the infimum equals the infimum of the sums a + b over b in s: a + sInf s = ⨅ b ∈ s, a + b.

Русский

Для множества s справедливо: a + sInf s = ⨅ b ∈ s, a + b.

LaTeX

$$$ a + \mathrm{sInf}\ s = \inf_{b \in s} (a + b) $$$

Lean4

theorem add_sInf {s : Set ℝ≥0∞} : a + sInf s = ⨅ b ∈ s, a + b := by rw [sInf_eq_iInf, add_iInf₂]

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

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

Разделы

Аффилиация

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