English
Union over an indexed family of sets s(i) equals the union of unions 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 \\bigcup_{i \\in \\iota} s(i) = \\bigcup_{t \\in \\mathrm{Finset}(\\iota)} \\bigcup_{i \\in t} s(i). $$$$
Lean4
/-- Union of an indexed family of sets `s : ι → Set α` is equal to the union of the unions
of finite subfamilies. This version assumes `ι : Type*`. See also `iUnion_eq_iUnion_finset'` for
a version that works for `ι : Sort*`. -/
theorem iUnion_eq_iUnion_finset (s : ι → Set α) : ⋃ i, s i = ⋃ t : Finset ι, ⋃ i ∈ t, s i :=
iSup_eq_iSup_finset s
