iSup₂_mono — Mathlib

English

Let α be a complete lattice and f,g : ι → κ i → α. If f i j ≤ g i j for all i and j, then ⨆ i (⨆ j, f i j) ≤ ⨆ i (⨆ j, g i j).

Русский

Пусть α — полная решетка и f,g : ι → κ i → α. Если f(i,j) ≤ g(i,j) для всех i, j, то ⨆ i ⨆ j f(i,j) ≤ ⨆ i ⨆ j g(i,j).

LaTeX

$$$\\\\forall i, j, f(i,j) \\\\le g(i,j) \\\\Rightarrow \\\\bigvee_{i} \\\\bigvee_{j} f(i,j) \\\\le \\\\bigvee_{i} \\\\bigvee_{j} g(i,j)$$$

Lean4

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

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