English
Let α be a type, p a property of subsets of α, and t a subset of α. If there exists a countable family S of subsets of α such that every element of S satisfies p and such that S separates points of t (i.e., for any x, y in t, if x and y have exactly the same membership pattern to all sets in S, then x = y), then such an S exists.
Русский
Пусть α — множество, p — свойство множест α, t ⊆ α. Если существует счетное семейство S подпосетов α, такое что каждый элемент удовлетворяет p и оно разделяет точки t (если для x, y ∈ t их членство во всех s ∈ S совпадает, то x = y), то такое S существует.
LaTeX
$$$$\\exists S \\subseteq \\mathcal P(\\alpha),\\; \\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_countable_separating (α : Type*) (p : Set α → Prop) (t : Set α) [h : HasCountableSeparatingOn α p t] :
∃ S : Set (Set α), S.Countable ∧ (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y :=
h.1
