Typeclass for indiscrete topology

Stream: Is there code for X?

[Aaron Liu]

Something like this:

import Mathlib

class IndiscreteTopology (X : Type*) [t : TopologicalSpace X] : Prop where
  eq_top : t = ⊤

Do we have it? If we don't, do we want to have it?

[Kevin Buzzard]

Is it useful? I think the discrete topology is a lot more common.

[Aaron Liu]

Recently Just now I found myself wanting this, because a lot of theorems are true assuming the indiscrete topology. It's equivalent to Subsingleton (SeparationQuotient X) and I'm in the middle of generalizing some theorems to non-T0 spaces.

[Aaron Liu]

Maybe I'll come back to this if I need it again but for now I found a way around.

[Edward van de Meent]

a quick loogle search says there is no such thing in mathlib... the only relevant things i could find were docs#induced_const and docs#induced_top

[Edward van de Meent]

my query was loogle TopologicalSpace, ?t = ⊤

[Yaël Dillies]

@loogle (⊤ : TopologicalSpace _)

[loogle]

:search: continuous_top, nhds_top, and 11 more