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