1 parent 70088e5 commit c854586Copy full SHA for c854586
1 file changed
Mathlib/Topology/Order/Separable.lean
@@ -21,6 +21,8 @@ In this file we prove some results about a separable linearly ordered topologica
21
points of a subset that are isolated in the subspace topology form a countable set.
22
* `Set.separableSpace`: a separable linearly ordered topological space is hereditarily separable.
23
24
+TODO: Generalize the hereditary separability result to separable GO-spaces.
25
+
26
-/
27
28
public section
0 commit comments