iSup_mul_iSup_le — Mathlib

English

If for all i, j, g(i) · h(j) ≤ a, then (sup_i g(i)) · (sup_j h(j)) ≤ a.

Русский

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

LaTeX

$$$ \\big(\\sup_{i \\in \\iota} g(i)\\big) \\cdot \\big(\\sup_{j \\in \\iota} h(j)\\big) \\le a $$$

Lean4

theorem iSup_mul_iSup_le {a : ℝ≥0} {g h : ι → ℝ≥0} (H : ∀ i j, g i * h j ≤ a) : iSup g * iSup h ≤ a :=
  iSup_mul_le fun _ => mul_iSup_le <| H _

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