Commit 2025-08-29 09:05 09a71ca7

View on Github →

feat: nontriviality of SeparationQuotient iff the topology is nontrivial (#28102) This contains the mathematical content of #Is there code for X? > Typeclass for nontrivial topology @ 💬, without yet committing to any designated API to make it easier to use.

Estimated changes

Modified Mathlib/Topology/Inseparable.lean

added theorem SeparationQuotient.inseparableSetoid_eq_top_iff

added theorem SeparationQuotient.nontrivial_iff

added theorem SeparationQuotient.subsingleton_iff

Modified Mathlib/Topology/Order.lean

added theorem TopologicalSpace.eq_top_iff_forall_inseparable

added theorem TopologicalSpace.ne_top_iff_exists_not_inseparable

added theorem inseparable_top