Theorem SeparationQuotient.inseparableSetoid_eq_top_iff

Modification history

2026-01-28 19:17
Mathlib/Topology/Inseparable.lean
feat: add a typeclass for the indiscrete topology (#29120) …
Modified SeparationQuotient.inseparableSetoid_eq_top_iffView on Github →
2025-08-29 09:05
Mathlib/Topology/Inseparable.lean
feat: nontriviality of `SeparationQuotient` iff the topology is nontrivial (#28102) …
Added SeparationQuotient.inseparableSetoid_eq_top_iffView on Github →