English
Let f: ∀ i, κ i → α be a family of elements in a complete lattice. The double supremum ∨_{i} ∨_{j} f(i,j) equals ⊤ if and only if for every b < ⊤ there exist i and j with b < f(i,j).
Русский
Пусть f: ∀ i, κ i → α — семейство элементов в полной решетке. Двойная верхняя граница ∨_{i} ∨_{j} f(i,j) равна ⊤ тогда и только тогда, когда для каждого b < ⊤ существуют i и j, такие что b < f(i,j).
LaTeX
$$$\\displaystyle \\big\\vee_{i} \\big\\vee_{j} f(i,j) = \\top \\iff \\forall b < \\top, \\exists i, \\exists j, b < f(i,j)$$$
Lean4
theorem iSup₂_eq_top (f : ∀ i, κ i → α) : ⨆ i, ⨆ j, f i j = ⊤ ↔ ∀ b < ⊤, ∃ i j, b < f i j := by
simp_rw [iSup_psigma', iSup_eq_top, PSigma.exists]
