Theorems · Inductive type · general topology

HasCountableSeparatingOn

(α : Type u_1) → (Set α → Prop) → Set α → Prop

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

Cited by

23 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms