Looking to contribute Polish spaces

Stream: new members

[Carlos Silva]

Regarding the metrizable bit, I looked at some theorems involving Polish spaces, and it looks like most of them have a formula for the complete metric. Thus it might be fine to define a “Polish metric space," which is just a metric space that is complete and separable.

I will think about the pros and cons of metrizability later. I'll go look at the topology section and see what ways I can express Polish spaces.

[Patrick Massot]

Johan, you're making it much more complicated than needed:

class polish_space (X : Type*) [t : uniform_space X]
  extends separable_space X, complete_space X :=
(metrizable : ∃ m : metric_space X, m.to_uniform_space = t)

[Patrick Massot]

My recommendation is to prove all lemmas simply for complete metric space and worry about polish spaces only when dealing with examples.

[Patrick Massot]

This declaration can be useful if you indeed have a type which already has a topology and you want to prove it's metrizable.

[Johan Commelin]

@Patrick Massot I wasn't sure whether we wanted to assume uniform_space or merely topological_space.

[Sebastien Gouezel]

You definitely only want to assume a topology, not a uniform structure.

[Johan Commelin]

Apparently #8759 added metrizable spaces. (I missed that PR. Holidays :grinning:)

[Johan Commelin]

But not as a typeclass, apparently.