English
For a finite s and t, the double supremum over the sigma-structure equals the iterated supremum: the supremum over all ij ∈ s.sigma t of f ij equals the supremum over i ∈ s and j ∈ t i of f ⟨i,j⟩.
Русский
Для конечного s и t постройка сигмы дает равенство двух операций взятия верхней границей: наибольшая величина по всем парам ij ∈ s.sigma t равна поочередному применения верхней границы по i ∈ s, затем по j ∈ t i.
LaTeX
$$$$ \bigvee_{ij \in s.sigma t} f(ij) = \bigvee_{i \in s} \bigvee_{j \in t(i)} f(\langle i,j \rangle) $$$$
Lean4
theorem _root_.biSup_finsetSigma [CompleteLattice β] (s : Finset ι) (t : ∀ i, Finset (α i)) (f : Sigma α → β) :
⨆ ij ∈ s.sigma t, f ij = ⨆ (i ∈ s) (j ∈ t i), f ⟨i, j⟩ := by
simp_rw [← Finset.iSup_coe, Finset.coe_sigma, biSup_sigma]
