English
Under the same assumptions as the previous statement, there exists a countable separating family S of p-subsets which is nonempty, and which separates points of t.
Русский
При тех же предпосылках существует счетное разделяющее семейство S подмножеств, удовлетворяющих p, которое непусто и отделяет точки t.
LaTeX
$$$$\\exists S \\subseteq \\mathcal P(\\alpha),\\; S \\neq \\varnothing \\land \\operatorname{Countable}(S) \\land (\\forall s \\in S, p(s)) \\land \\forall x \\in t, \\forall y \\in t, (\\forall s \\in S, x \\in s \\iff y \\in s) \\Rightarrow x = y.$$$$
Lean4
theorem exists_nonempty_countable_separating (α : Type*) {p : Set α → Prop} {s₀} (hp : p s₀) (t : Set α)
[HasCountableSeparatingOn α p t] :
∃ S : Set (Set α), S.Nonempty ∧ S.Countable ∧ (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y :=
let ⟨S, hSc, hSp, hSt⟩ := exists_countable_separating α p t
⟨insert s₀ S, insert_nonempty _ _, hSc.insert _, forall_insert_of_forall hSp hp, fun x hx y hy hxy ↦
hSt x hx y hy <| forall_of_forall_insert hxy⟩
