Theorems · Theorem · logic and foundations

Set.exists_seq_cover_iff_countable

∀ {α : Type u} {p : Set α → Prop},
  (∃ s, p s) → ((∃ s, (∀ (n : ℕ), p (s n)) ∧ ⋃ n, s n = Set.univ) ↔ ∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ ⋃₀ S = Set.univ)

Defined in

Mathlib.Data.Set.Countable

Cited by

2 results in Mathlib

Foundations

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