Theorems · Theorem · order theory

Set.eq_finite_iUnion_of_finite_subset_iUnion

∀ {α : Type u} {ι : Type u_1} {s : ι → Set α} {t : Set α},
  t.Finite →
    t ⊆ ⋃ i, s i →
      ∃ I, I.Finite ∧ ∃ σ, (∀ (i : ↑{i | i ∈ I}), (σ i).Finite) ∧ (∀ (i : ↑{i | i ∈ I}), σ i ⊆ s ↑i) ∧ t = ⋃ i, σ i

Defined in

Mathlib.Data.Set.Finite.Lattice

Cited by

1 results in Mathlib

Foundations

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