biInter_finsetSigma' — Mathlib

English

A prime variant of the previous Set Inter Sigma identity; the nested intersections decompose along the sigma structure.

Русский

Прайм-вариант идентичности пересечений над сигмой; вложенные пересечения распадаются вдоль сигма-структуры.

LaTeX

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

Lean4

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

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