## Stream: maths

### Topic: discrete spaces

#### Reid Barton (Oct 18 2018 at 23:01):

feat(analysis/topology): add type class for discrete topological spaces
feat(analysis/topology): add type class for discrete topological spaces
https://github.com/leanprover/mathlib/commit/f6812d5a881b1bca826808e6bd40eb3e75979d2a

@Johannes Hölzl nice! This is something I was also considering adding, compare https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.1/src/for_mathlib/analysis_topology_topological_space.lean. I was thinking of making it an alternative branch in the topological_space <- uniform_space <- metric_space chain; in the link I put it on top of topological_space but it could easily go on top of uniform_space instead.
Thoughts?

#### Reid Barton (Oct 18 2018 at 23:04):

The advantage is that you wouldn't need all those separate instances for spaces like nat--the disadvantage is you have to be a bit careful to define the instances for things like products and sums correctly, I guess.

#### Johannes Hölzl (Oct 19 2018 at 07:25):

I wonder if there exists a case where we have a discrete topology, but one still additional topological structures on it. For example orderable_topology doesn't hold for all discrete spaces. Of course orderable_topology is a mixin in itself so it would fit. But I prefer the flexibility we get from mixins. And I guess discrete_topology isn't used too often so writing two parameters instead of one shouldn't be too hard.
Hence, I would like to keep it as an mixin (i.e. a predicate, not containing the toplogical structure).

#### Reid Barton (Oct 19 2018 at 13:54):

Ah, I see. I can imagine a situation where you have a manifold or a topological ring or something, and then also want to assume or prove that the topology is discrete. Makes sense.

Last updated: May 19 2021 at 00:40 UTC