mathlib

9f55d0d4 - feat(measure_theory/constructions/polish): quotient group is a Borel space (#19186)

feat(measure_theory/constructions/polish): quotient group is a Borel space (#19186) * Suslin's theorem: an analytic set with analytic complement is measurable. * Image of a measurable set in a Polish space under a measurable map is an analytic set. * Preimage of a set under a measurable surjective map from a Polish space is measurable iff the original set is measurable. * Quotient space of a Polish space with quotient σ-algebra is a Borel space provided that it has second countable topology. * In particular, quotient group of a Polish topological group is a Borel space. * Change instance for `measurable_space` on `add_circle`.