Theorem TopologicalSpace.ne_top_iff_exists_not_inseparable

Modification history

2025-08-29 09:05
Mathlib/Topology/Order.lean
feat: nontriviality of `SeparationQuotient` iff the topology is nontrivial (#28102) …
Added TopologicalSpace.ne_top_iff_exists_not_inseparableView on Github →