Theorems · Theorem · order theory

Set.finite_iUnion_iff

∀ {α : Type u} {ι : Type u_1} {s : ι → Set α},
  (Pairwise fun i j => Disjoint (s i) (s j)) →
    ((⋃ i, s i).Finite ↔ (∀ (i : ι), (s i).Finite) ∧ {i | (s i).Nonempty}.Finite)

An indexed union of pairwise disjoint sets is finite iff all sets are finite, and all but finitely many are empty.

Defined in

Mathlib.Data.Set.Finite.Lattice

Cited by

2 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound