iInter_psigma — Mathlib

English

Let s : PSigma γ → Set β. Then the intersection over the PSigma index equals the iterated intersection: ⋂ ia, s ia = ⋂ i, ⋂ a, s ⟨i, a⟩.

Русский

Пусть s : PSigma γ → Set β. Тогда пересечение по PSigma-индексу равно последовательному пересечению: ⋂ 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_psigma {γ : α → Type*} (s : PSigma γ → Set β) : ⋂ ia, s ia = ⋂ i, ⋂ a, s ⟨i, a⟩ :=
  iInf_psigma _

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