Theorems · Theorem · logic and foundations

Set.countable_ofPred_nonempty_of_disjoint

∀ {α : Type u} {β : Type v} {f : β → Set α},
  Pairwise (Function.onFun Disjoint f) →
    ∀ {s : Set α}, (∀ (t : β), f t ⊆ s) → s.Countable → {t | (f t).Nonempty}.Countable

If a family of disjoint sets is included in a countable set, then only countably many of them are nonempty.

Defined in

Mathlib.Data.Set.Countable

Cited by

2 results in Mathlib

Foundations

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