English
There exists a sequence of subsets S_n of α such that every S_n satisfies p, and these sets separate points of t: if x and y in t have the same membership pattern across all S_n, then x = y.
Русский
Существует последовательность подмножеств S_n ⊆ α такая, что каждый S_n удовлетворяет p, и эти множества разделяют точки t: если для двух элементов x, y ∈ t их принадлежность к каждому S_n одинакова, то x = y.
LaTeX
$$$$\\exists S:\\mathbb N \\to \\mathcal P(\\alpha),\\; (\\forall n, S(n) \\text{ satisfies } p) \\land \\forall x\\in t, \\forall y\\in t, (\\forall n, x\\in S(n) \\iff y\\in S(n)) \\Rightarrow x = y.$$$$
Lean4
theorem exists_seq_separating (α : Type*) {p : Set α → Prop} {s₀} (hp : p s₀) (t : Set α)
[HasCountableSeparatingOn α p t] :
∃ S : ℕ → Set α, (∀ n, p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ n, x ∈ S n ↔ y ∈ S n) → x = y :=
by
rcases exists_nonempty_countable_separating α hp t with ⟨S, hSne, hSc, hS⟩
rcases hSc.exists_eq_range hSne with ⟨S, rfl⟩
use S
simpa only [forall_mem_range] using hS
