Theorem SeparationQuotient.nontrivial_iff

Modification history

2026-01-28 19:17

Mathlib/Topology/Inseparable.lean

feat: add a typeclass for the indiscrete topology (#29120) …

Modified SeparationQuotient.nontrivial_iff View on Github →

2025-08-29 09:05

Mathlib/Topology/Inseparable.lean

feat: nontriviality of `SeparationQuotient` iff the topology is nontrivial (#28102) …

Added SeparationQuotient.nontrivial_iff View on Github →