iInter_sigma — Mathlib

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

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