Theorem TopologicalSpace.eq_top_iff_forall_inseparable

Modification history

2026-08-11 12:14
Mathlib/Topology/Order.lean
chore: delete deprecated declarations/modules from January 2026 (#42075) …
Deleted TopologicalSpace.eq_top_iff_forall_inseparableView on Github →
2025-08-29 09:05
Mathlib/Topology/Order.lean
feat: nontriviality of `SeparationQuotient` iff the topology is nontrivial (#28102) …
Added TopologicalSpace.eq_top_iff_forall_inseparableView on Github →