iSup₂_le — Mathlib

English

For κ: ι → Sort* and a function f: ι → α, the double-index supremum is bounded above by the single supremum: ⨆ (i) (_ : κ i), f i ≤ ⨆ i, f i.

Русский

Для κ: ι → Sort и f: ι → α справедливо: ⨆ (i) (_ : κ i), f i ≤ ⨆ i, f i.

LaTeX

$$$$\\big\\lvert\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\; \\text{(двойная индексация)} \\; \\le \\; \\iSup_i f(i).$$$$

Lean4

theorem iSup₂_le {f : ∀ i, κ i → α} (h : ∀ i j, f i j ≤ a) : ⨆ (i) (j), f i j ≤ a :=
  iSup_le fun i => iSup_le <| h i

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