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 @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Typeclass.20for.20nontrivial.20topology/near/533192558), without yet committing to any designated API to make it easier to use.

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: eric-wieser

Mathlib/Topology/Inseparable.lean

@@ -556,6 +556,12 @@ theorem continuous_mk : Continuous (mk : X → SeparationQuotient X) :=
 theorem mk_eq_mk : mk x = mk y ↔ (x ~ᵢ y) :=
   Quotient.eq''
 
+protected theorem «forall» {P : SeparationQuotient X → Prop} : (∀ x, P x) ↔ ∀ x, P (.mk x) :=
+  Quotient.forall
+
+protected theorem «exists» {P : SeparationQuotient X → Prop} : (∃ x, P x) ↔ ∃ x, P (.mk x) :=
+  Quotient.exists
+
 theorem surjective_mk : Surjective (mk : X → SeparationQuotient X) :=
   Quot.mk_surjective
 
@@ -572,6 +578,19 @@ instance [Inhabited X] : Inhabited (SeparationQuotient X) :=
 instance [Subsingleton X] : Subsingleton (SeparationQuotient X) :=
   surjective_mk.subsingleton
 
+@[simp]
+theorem inseparableSetoid_eq_top_iff {t : TopologicalSpace α} :
+    inseparableSetoid α = ⊤ ↔ t = ⊤ :=
+  Setoid.eq_top_iff.trans TopologicalSpace.eq_top_iff_forall_inseparable.symm
+
+theorem subsingleton_iff {t : TopologicalSpace α} :
+    Subsingleton (SeparationQuotient α) ↔ t = ⊤ :=
+  Quotient.subsingleton_iff.trans inseparableSetoid_eq_top_iff
+
+theorem nontrivial_iff {t : TopologicalSpace α} :
+    Nontrivial (SeparationQuotient α) ↔ t ≠ ⊤ := by
+  simpa only [not_subsingleton_iff_nontrivial] using subsingleton_iff.not
+
 @[to_additive] instance [One X] : One (SeparationQuotient X) := ⟨mk 1⟩
 
 @[to_additive (attr := simp)] theorem mk_one [One X] : mk (1 : X) = 1 := rfl

Mathlib/Topology/Order.lean

@@ -618,6 +618,21 @@ theorem isOpen_sup {t₁ t₂ : TopologicalSpace α} {s : Set α} :
     IsOpen[t₁ ⊔ t₂] s ↔ IsOpen[t₁] s ∧ IsOpen[t₂] s :=
   Iff.rfl
 
+/-- In the trivial topology no points are separable.
+
+The corresponding `bot` lemma is handled more generally by `inseparable_iff_eq`. -/
+@[simp]
+theorem inseparable_top (x y : α) : @Inseparable α ⊤ x y := nhds_top.trans nhds_top.symm
+
+theorem TopologicalSpace.eq_top_iff_forall_inseparable {t : TopologicalSpace α} :
+    t = ⊤ ↔ (∀ x y : α, Inseparable x y) where
+  mp h := h ▸ inseparable_top
+  mpr h := ext_nhds fun x => nhds_top ▸ top_unique fun _ hs a => mem_of_mem_nhds <| h x a ▸ hs
+
+theorem TopologicalSpace.ne_top_iff_exists_not_inseparable {t : TopologicalSpace α} :
+    t ≠ ⊤ ↔ ∃ x y : α, ¬Inseparable x y := by
+  simpa using eq_top_iff_forall_inseparable.not
+
 open TopologicalSpace
 
 variable {γ : Type*} {f : α → β} {ι : Sort*}