Theorems · Inductive type · general topology

TopologicalSpace.SeparableSpace

(α : Type u) → [t : TopologicalSpace α] → Prop

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

Cited by

109 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

TopologicalSpace