English
For a family of sets indexed by ι, the union ⋃ i s i is finite iff each s i is finite and the set of indices with nonempty s i is finite, provided the index family is pairwise disjoint.
Русский
Для семейства множеств s i индексированного ι объединение ⋃ i s i конечно тогда и только тогда, когда каждое s i конечно и множество индексов с непустыми s i конечно, при условии попарной непересечения.
LaTeX
$$$\\operatorname{Finite}\\left(\\bigcup_i s_i\\right) \\iff \\left(\\forall i, \\operatorname{Finite}(s_i) \\right) \\land \\{i \\mid (s_i).Nonempty\\}.\\Finite$$
Lean4
/-- An indexed union of pairwise disjoint sets is finite iff all sets are finite, and all but
finitely many are empty. -/
theorem finite_iUnion_iff {ι : Type*} {s : ι → Set α} (hs : Pairwise fun i j ↦ Disjoint (s i) (s j)) :
(⋃ i, s i).Finite ↔ (∀ i, (s i).Finite) ∧ {i | (s i).Nonempty}.Finite
where
mp
h := by
refine ⟨fun i ↦ h.subset <| subset_iUnion _ _, ?_⟩
let u (i : {i | (s i).Nonempty}) : ⋃ i, s i := ⟨i.2.choose, mem_iUnion.2 ⟨i.1, i.2.choose_spec⟩⟩
have u_inj : Function.Injective u := by
rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
ext
refine hs.eq <| not_disjoint_iff.2 ⟨u ⟨i, hi⟩, hi.choose_spec, ?_⟩
rw [hij]
exact hj.choose_spec
have : Finite (⋃ i, s i) := h
exact .of_injective u u_inj
mpr h := h.2.iUnion (fun _ _ ↦ h.1 _) (by simp [not_nonempty_iff_eq_empty])
