Structures · Order

HasCountableSeparatingOn

We say that a type α has a countable separating family of sets satisfying a predicate p : Set α → Prop on a set t if there exists a countable family of sets S : Set (Set α) such that all sets s ∈ S satisfy p and any two distinct points x y ∈ t, x ≠ y, can be separated by s ∈ S: there exists s ∈ S such that exactly one of x and y belongs to s. E.g., if α is a T₀ topological space with second countable topology, then it has a countable separating family of open sets and a countable separating family of closed sets.

Defined in

Mathlib.Order.Filter.CountableSeparatingOn

Shape

3 explicit arguments · adds exists_countable_separating