Theorems · Definition · general topology

TopologicalSpace.IsSeparable

{α : Type u} → [t : TopologicalSpace α] → Set α → Prop

A set s in a topological space is separable if it is contained in the closure of a countable set c. Beware that this definition does not require that c is contained in s (to express the latter, use TopologicalSpace.SeparableSpace s or TopologicalSpace.IsSeparable (univ : Set s)). In metric spaces, the two definitions are equivalent, see TopologicalSpace.IsSeparable.separableSpace.

Defined in

Mathlib.Topology.Bases

Cited by

51 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

TopologicalSpace