ciSup_mul_ciSup_le — Mathlib

English

If g(i)·h(j) ≤ a for all i and j, then the supremum of g times the supremum of h is ≤ a.

Русский

Если ∀i,j: g(i)·h(j) ≤ a, то (sup_i g(i))·(sup_j h(j)) ≤ a.

LaTeX

$$$\displaystyle \forall i,\forall 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_ciSup_le [MulLeftMono α] [MulRightMono α] {a : α} {g : ι → α} {h : ι' → α}
    (H : ∀ i j, g i * h j ≤ a) : iSup g * iSup h ≤ a :=
  ciSup_mul_le fun _ => mul_ciSup_le <| H _

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