English
For s ⊆ ι, t: ∀ i, Set(α i), and f: Σ i α i → β in a complete lattice β, the supremum over ij ∈ s.sigma t of f(ij) equals the supremum over i ∈ s and j ∈ t(i) of f(⟨i,j⟩).
Русский
Пусть s ⊆ ι, t: ∀ i, Set(α i), и f: Σ i α i → β в полной полудеже. Тогда наибольшая верхняя грань по всем парам (i,j) с i ∈ s и j ∈ t(i) равна наибольшей верхней грани по всем i ∈ s и j ∈ t(i) от f(⟨i,j⟩).
LaTeX
$$$\bigsqcup_{ij \in s \sigma t} f(ij) = \bigsqcup_{i \in s} \bigsqcup_{j \in t(i)} f(\langle i,j\rangle)$$$
Lean4
theorem _root_.biSup_sigma (s : Set ι) (t : ∀ i, Set (α i)) (f : Sigma α → β) :
⨆ ij ∈ s.sigma t, f ij = ⨆ (i ∈ s) (j ∈ t i), f ⟨i, j⟩ :=
eq_of_forall_ge_iff fun _ ↦ ⟨by simp_all, by simp_all⟩
