English
An indexed union of pairwise disjoint sets is finite iff all sets are finite and only finitely many are nonempty.
Русский
Индексированное объединение взаимно непересекающихся множеств конечно тогда и только тогда, когда все множества конечны и осталось конечное число непустых.
LaTeX
$$$\\operatorname{Finite}\\left(\\bigcup i \\in s, f(i)\\right) \\iff (\\forall i \\in s, \\operatorname{Finite}(f(i))) \\land \\{ i \\in s \\,|\\, (f(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_biUnion_iff {f : β → Set α} {s : Set β} (hs : s.PairwiseDisjoint f) :
(⋃ i ∈ s, f i).Finite ↔ (∀ i ∈ s, (f i).Finite) ∧ {i ∈ s | (f i).Nonempty}.Finite :=
by
rw [finite_iUnion_iff (by aesop (add unfold safe [Pairwise, PairwiseDisjoint, Set.Pairwise]))]
simp
