Theorem TopologicalSpace.nontrivial_iff_exists_not_inseparable

Modification history

2026-01-28 19:17
Mathlib/Topology/Order.lean
feat: add a typeclass for the indiscrete topology (#29120) …
Added TopologicalSpace.nontrivial_iff_exists_not_inseparableView on Github →