English
For families u and v indexed by a 2-parameter index (i,j), the supremum of the products u(i,j) v(i,j) is bounded above by the product of the suprema of u and v separately.
Русский
Для парных индексов u(i,j) и v(i,j) верхняя грань произведения не превосходит произведения верхних границ по каждой координате.
LaTeX
$$$$ \\sup_{i,j} \\big( u(i,j) \\cdot v(i,j) \\big) \\le \\left( \\sup_{i,j} u(i,j) \\right) \\cdot \\left( \\sup_{i,j} v(i,j) \\right) $$$$
Lean4
@[to_additive]
theorem iSup₂_mul_le (u v : (i : ι) → κ i → α) : ⨆ (i) (j), u i j * v i j ≤ (⨆ (i) (j), u i j) * ⨆ (i) (j), v i j :=
by
refine le_trans ?_ (iSup_mul_le ..)
gcongr
exact iSup_mul_le ..
