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