iSup_comm — Mathlib

English

Supremum over a two-parameter index can be swapped: ⨆ i (j) f(i,j) = ⨆ j (i) f(i,j).

Русский

Супремум по паре индексов можно поменять местами: ⨆_{i}⨆_{j} f(i,j) = ⨆_{j}⨆_{i} f(i,j).

LaTeX

$$$$\bigvee_{i} \bigvee_{j} f(i,j) = \bigvee_{j} \bigvee_{i} f(i,j).$$$$

Lean4

theorem iSup_comm {f : ι → ι' → α} : ⨆ (i) (j), f i j = ⨆ (j) (i), f i j :=
  le_antisymm (iSup_le fun i => iSup_mono fun j => le_iSup (fun i => f i j) i)
    (iSup_le fun _ => iSup_mono fun _ => le_iSup _ _)

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