English
There exists a sequence of sets that covers the universe iff there exists a countable collection of sets whose union is the universe with each member satisfying p.
Русский
Существует последовательность множеств, покрывающая вселенную, тогда и только тогда существует счетное множество множеств, чья объединение равно вселенной и каждое множество удовлетворяет условию.
LaTeX
$$$\\exists s:\\mathbb{N}\\to \\mathcal P(\\alpha), (\\forall n, p(s(n))) \\land \\bigcup_n s(n) = \\mathrm{univ} \\iff \\exists S:\\Set(\\mathcal P(\\alpha)), S.Countable \\land (\\forall s\\in S, p(s)) \\land \\bigcup S = \\mathrm{univ}$$$
Lean4
theorem exists_seq_cover_iff_countable {p : Set α → Prop} (h : ∃ s, p s) :
(∃ s : ℕ → Set α, (∀ n, p (s n)) ∧ ⋃ n, s n = univ) ↔
∃ S : Set (Set α), S.Countable ∧ (∀ s ∈ S, p s) ∧ ⋃₀ S = univ :=
exists_seq_iSup_eq_top_iff_countable h
