Theorems · Theorem · order theory

Set.Finite.iUnion

∀ {α : Type u} {ι : Type u_1} {s : ι → Set α} {t : Set ι},
  t.Finite → (∀ i ∈ t, (s i).Finite) → (∀ i ∉ t, s i = ∅) → (⋃ i, s i).Finite

If sets s i are finite for all i from a finite set t and are empty for i ∉ t, then the union ⋃ i, s i is a finite set.

Defined in

Mathlib.Data.Set.Finite.Lattice

Cited by

2 results in Mathlib

Foundations

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