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

[Eric Wieser]

I found myself wanting this too; we have a few lemmas using ∃ x, ‖x‖ ≠ 0 for seminormed spaces which end up with API duplication for nontrivial normed spaces.

[Eric Wieser]

Oh, I guess I wanted NotIndiscrete

[Notification Bot]

2 messages were moved from this topic to #Is there code for X? > Typeclass for nontrivial topology by Eric Wieser.

[Notification Bot]

A message was moved here from #Is there code for X? > Typeclass for nontrivial topology by Eric Wieser.

[Eric Wieser]

Though in fact I'd quite like both, as a nicer way to spell cases subsingleton_or_nontrivial (SeparationQuotient X)