biInter_finsetSigma — Mathlib

English

The intersection over ij ∈ s.sigma t of a family equals the intersection over i ∈ s and j ∈ t i of the corresponding families.

Русский

Пересечение по ij ∈ s.sigma t семейства равно пересечению по i ∈ s и j ∈ t i соответствующих семейств.

LaTeX

$$$$ \bigcap_{ij \in s.sigma t} f(ij) = \bigcap_{i \in s} \bigcap_{j \in t_i} f(\langle i,j\rangle) $$$$

Lean4

theorem _root_.Set.biInter_finsetSigma (s : Finset ι) (t : ∀ i, Finset (α i)) (f : Sigma α → Set β) :
    ⋂ ij ∈ s.sigma t, f ij = ⋂ i ∈ s, ⋂ j ∈ t i, f ⟨i, j⟩ :=
  biInf_finsetSigma _ _ _

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