[Merged by Bors] - feat(measure_theory/constructions/polish): quotient group is a Borel space

[urkud]

• 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.

---

[sgouezel]

bors r+ Thanks!

[bors[bot]]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests