English
For a family of sets f on Sigma α, the union over ij ∈ s.sigma t of f ij equals the union over i ∈ s and j ∈ t i of f ⟨i, j⟩.
Русский
Для семейства множеств f на Σα объединение по ij ∈ s.sigma t равно объединению по i ∈ s и j ∈ t i от f ⟨i, j⟩.
LaTeX
$$$$ \\bigcup_{ij \\in s.sigma t} f(ij) = \\bigcup_{i \\in s} \\bigcup_{j \\in t(i)} f(\\langle i,j\\rangle) $$$$
Lean4
theorem _root_.Set.biUnion_finsetSigma (s : Finset ι) (t : ∀ i, Finset (α i)) (f : Sigma α → Set β) :
⋃ ij ∈ s.sigma t, f ij = ⋃ i ∈ s, ⋃ j ∈ t i, f ⟨i, j⟩ :=
biSup_finsetSigma _ _ _