## Stream: maths

### Topic: sober spaces

#### Johan Commelin (Feb 05 2020 at 17:58):

https://en.wikipedia.org/wiki/Sober_space
A sober space is a topological space in which every irreducible (i.e. nonempty preirreducible) subset Z has a unique generic point: i.e. there is a unique x in Z such that Z is the closure of {x}.

I'm thinking of introducing sober_space as a class. Should it be a predicate, or should it carry a function that provides the generic point? I think in practice this function will never be computable, so I'm inclided to go for the predicate version.

#### Jeremy Avigad (Feb 06 2020 at 20:10):

The terminology gave rise to one of my favorite paper titles: https://link.springer.com/chapter/10.1007%2FBFb0089911. "Scott" here is Dana Scott, who first told me about it.

#### Reid Barton (May 03 2020 at 20:33):

I think the Prop version is fine.

#### Patrick Massot (May 03 2020 at 21:03):

Reid, did you really intend to post this message in that old thread?

#### Kevin Buzzard (May 03 2020 at 21:08):

Maybe he wants them too and realised we still don't have them :-)

#### Patrick Massot (May 03 2020 at 21:14):

Do you mean he actually is continuing that thread?

#### Patrick Massot (May 03 2020 at 21:14):

I didn't even read Johan's message, I assumed Reid messed up with Zulip.