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' _ _ _