iUnion_psigma — Mathlib

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 _

Похожие утверждения