le_mul_iInf

Mathlib.Data.NNReal.Basic

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

English

If for all j, a ≤ g · h(j), then a ≤ g · inf_j h(j).

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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