English
For γ: α → Type*, and s : Sigma γ → Set β, the union over ia of s ia equals the union over i and a of s ⟨i,a⟩.
Русский
Для γ: α → Type*, и S: Sigma γ → Set β, объединение по ia равно объединению по i и a: ⋃ ia, s ia = ⋃ i, ⋃ a, s ⟨i,a⟩.
LaTeX
$$$$\\bigcup_{ia} s_{ia} = \\bigcup_{i} \\bigcup_{a} s_{\\langle i,a\\rangle}$$$$
Lean4
theorem iUnion_sigma {γ : α → Type*} (s : Sigma γ → Set β) : ⋃ ia, s ia = ⋃ i, ⋃ a, s ⟨i, a⟩ :=
iSup_sigma