isLUB_ciSup_set — Mathlib

English

If g(i)·h(j) ≤ a for all i and j, then the product of the suprema 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,\forall j,\ g(i)\cdot h(j) \le a \quad\Rightarrow\quad (\sup_i g(i))\cdot (\sup_j h(j)) \le a$$$

Lean4

theorem isLUB_ciSup_set {f : β → α} {s : Set β} (H : BddAbove (f '' s)) (Hne : s.Nonempty) :
    IsLUB (f '' s) (⨆ i : s, f i) := by
  rw [← sSup_image']
  exact isLUB_csSup (Hne.image _) H

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