Commit 2025-10-24 20:19 39cfbec5
View on Github →feat: if the order topology for a dense linear ordering is discrete, the space has at most one point (#30856) See also Zulip discussion
feat: if the order topology for a dense linear ordering is discrete, the space has at most one point (#30856) See also Zulip discussion