sInf_add

Mathlib.Data.ENNReal.Operations

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

English

For any set s, the infimum of the sums with a fixed a equals the sum with aInf: sInf s + a = ⨅ b ∈ s, b + a.

Русский

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

LaTeX

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

Lean4

theorem sInf_add {s : Set ℝ≥0∞} : sInf s + a = ⨅ b ∈ s, b + a := by simp [sInf_eq_iInf, iInf_add]

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

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

Разделы

Аффилиация

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