le_iInf_mul_iInf — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem le_iInf_mul_iInf {a : ℝ≥0} {g h : ι → ℝ≥0} (H : ∀ i j, a ≤ g i * h j) : a ≤ iInf g * iInf h :=
  le_iInf_mul fun i => le_mul_iInf <| H i

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