Theorems · Theorem · logic and foundations

Set.exists_seq_iSup_eq_top_iff_countable

∀ {α : Type u} [inst : CompleteLattice α] {p : α → Prop},
  (∃ x, p x) → ((∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤) ↔ ∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤)

Defined in

Mathlib.Data.Set.Countable

Cited by

1 results in Mathlib

Foundations

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

Assumes

CompleteLattice