add_iInf_le_iInf_add

Mathlib.Topology.Instances.EReal.Lemmas

URI: https://scilib.ai/kg/mathlib#EReal.add_iInf_le_iInf_add

English

The infimum over x of u(x) plus the infimum over x of v(x) is at most the infimum over x of (u(x)+v(x)).

Русский

Infimum по x от u(x) плюс infimum по x от v(x) не превосходит infimum по x от (u(x)+v(x)).

LaTeX

$$$ (\inf_{x} u(x)) + (\inf_{x} v(x)) \le \inf_{x} (u(x) + v(x)) $$$

Lean4

theorem add_iInf_le_iInf_add : (⨅ x, u x) + ⨅ x, v x ≤ ⨅ x, (u + v) x :=
  le_iInf fun i ↦ add_le_add (iInf_le u i) (iInf_le v i)

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

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

Разделы

Аффилиация

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