ciSup_mul_le — Mathlib

English

If g(i)·h(j) ≤ a for all i,j, then the product of the supremums is ≤ a: (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

$$$\displaystyle \forall i,j,\ g(i)\cdot h(j) \le a \quad\Rightarrow\quad (\sup_i g(i))\cdot (\sup_j h(j)) \le a$$$

Lean4

@[to_additive]
theorem ciSup_mul_le [MulRightMono α] {a : α} {g : ι → α} {h : α} (H : ∀ i, g i * h ≤ a) : iSup g * h ≤ a :=
  le_ciInf_mul (α := αᵒᵈ) H

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