iUnion_sigma — Mathlib

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

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