Structures · Topology

TopologicalSpace.SeparableSpace

A separable space is one with a countable dense subset, available through TopologicalSpace.exists_countable_dense. If α is also known to be nonempty, then TopologicalSpace.denseSeq provides a sequence ℕ → α with dense range, see TopologicalSpace.denseRange_denseSeq. If α is a uniform space with countably generated uniformity filter (e.g., an EMetricSpace), then this condition is equivalent to SecondCountableTopology α. In this case the latter should be used as a typeclass argument in theorems because Lean can automatically deduce TopologicalSpace.SeparableSpace from SecondCountableTopology using TopologicalSpace.SecondCountableTopology.to_separableSpace, but deducing SecondCountableTopology from TopologicalSpace.SeparableSpace requires more assumptions.

Defined in

Mathlib.Topology.Bases

Shape

One type argument · adds exists_countable_dense