English
For γ: α → Type*, and s : Σ γ → Set β, the intersection over ia of s ia equals the intersection over i and a of s ⟨i,a⟩.
Русский
Для γ: α → Type*, и s : Σ γ → Set β, пересечение по ia равно пересечению по i и a: ⋂ ia, s ia = ⋂ i, ⋂ a, s ⟨i,a⟩.
LaTeX
$$$$\\bigcap_{ia} s_{ia} = \\bigcap_{i} \\bigcap_{a} s_{\\langle i,a\\rangle}$$$$
Lean4
theorem iInter_sigma {γ : α → Type*} (s : Sigma γ → Set β) : ⋂ ia, s ia = ⋂ i, ⋂ a, s ⟨i, a⟩ :=
iInf_sigma