le_iInf_add_iInf

Mathlib.Data.ENNReal.Operations

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

English

If for all i,j we have a ≤ f(i) + g(j), then a ≤ iInf f + iInf g.

Русский

Если для всех i,j выполняется a ≤ f(i) + g(j), то a ≤ iInf f + iInf g.

LaTeX

$$$ a \le \inf_i f(i) + \inf_j g(j) $ given \forall i,j: a \le f(i) + g(j).$$

Lean4

theorem le_iInf_add_iInf {g : κ → ℝ≥0∞} (h : ∀ i j, a ≤ f i + g j) : a ≤ iInf f + iInf g := by
  simp_rw [iInf_add, add_iInf]; exact le_iInf₂ h

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

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

Разделы

Аффилиация

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