English
For a family of sets indexed by a PSigma type, the union over the PSigma index equals the iterated union over the first and second components: ⋃ ia, s ia = ⋃ i, ⋃ a, s ⟨i, a⟩.
Русский
Для семейства множеств, индексируемых по PSigma, объединение по PSigma-размножению равно поочередному объединению по первым и вторым компонентам: ⋃ 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_psigma {γ : α → Type*} (s : PSigma γ → Set β) : ⋃ ia, s ia = ⋃ i, ⋃ a, s ⟨i, a⟩ :=
iSup_psigma _