le_iInf_mul

Mathlib.Data.NNReal.Basic

URI: https://scilib.ai/kg/mathlib#NNReal.le_iInf_mul

English

If for all i, a ≤ g(i) · h, then a ≤ (inf_i g(i)) · h.

Русский

Если для всех i верно a ≤ g(i) · h, тогда a ≤ (inf_i g(i)) · h.

LaTeX

$$$ \\forall i,\\ a \\le g(i) \\cdot h \\quad \\Rightarrow\\quad a \\le \\big(\\inf_{i \\in \\iota} g(i)\\big) \\cdot h $$$

Lean4

theorem le_iInf_mul {a : ℝ≥0} {g : ι → ℝ≥0} {h : ℝ≥0} (H : ∀ i, a ≤ g i * h) : a ≤ iInf g * h :=
  by
  rw [iInf_mul]
  exact le_ciInf H

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

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

Разделы

Аффилиация

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