Do we need `separated_space`?

Stream: maths

[Yury G. Kudryashov]

We have two typeclasses, docs#t2_space and docs#separated_space. These propositions are equivalent but the latter needs a uniform space structure to be defined. Some lemmas assume [t2_space X], some assume [separated_space X]. I suggest that we drop separated_space and replace it with a custom constructor for t2_space.

[Sebastien Gouezel]

@Patrick Massot ?

[Yury G. Kudryashov]

@Patrick Massot ping here

[Patrick Massot]

I'm sorry I missed that one. I think this is a historical accident. This is very old code, from Johannes's time.

[Patrick Massot]

I assume we can safely drop separated_space (but it will require some work)

[Yury G. Kudryashov]

I'll try to do it.

[Yury G. Kudryashov]

How should I call the setoid that will unify docs#indistinguishable, docs#separation_rel, and docs#pseudo_metric.dist_setoid?

[Yury G. Kudryashov]

I'm going to define it as setoid.comap nhds ⊥

[Yury G. Kudryashov]

@Patrick Massot Do you have any preferences about the name?

[Patrick Massot]

I think that something involving separation or separated is better than indistinguishable that sounds nice but is too generic (topologically_indistinguishable is really too long and abbreviating it would probably make it very hard to decipher).

[Yury G. Kudryashov]

inseparable?