English
Intersection over an indexed family of sets s(i) with Sort indices equals the intersection of intersections over Finset (PLift ι') of the intersections s(PLift.down i).
Русский
Пересечение по семейству множеств с индексами типа Sort равно пересечению пересечений по Finset(PLift ι') от s(PLift.down i).
LaTeX
$$$$\\displaystyle \\bigcap_{i \\in \\iota'} s(i) = \\bigcap_{t \\in \\mathrm{Finset}(\\mathrm{PLift} \\iota')} \\bigcap_{i \\in t} s(\\mathrm{PLift.down} i). $$$$
Lean4
/-- Intersection of an indexed family of sets `s : ι → Set α` is equal to the intersection of the
intersections of finite subfamilies. This version works for `ι : Sort*`. See also
`iInter_eq_iInter_finset` for a version that assumes `ι : Type*` but avoids `PLift`s in the
right-hand side. -/
theorem iInter_eq_iInter_finset' (s : ι' → Set α) : ⋂ i, s i = ⋂ t : Finset (PLift ι'), ⋂ i ∈ t, s (PLift.down i) :=
iInf_eq_iInf_finset' s
