mathlib

2d6c52af - feat(topology/metric_space/polish): definition and basic properties of polish spaces (#12437)

feat(topology/metric_space/polish): definition and basic properties of polish spaces (#12437) A topological space is Polish if its topology is second-countable and there exists a compatible complete metric. This is the class of spaces that is well-behaved with respect to measure theory. In this PR, we establish basic (and not so basic) properties of Polish spaces.