Commit 2023-06-14 16:17 9f55d0d4

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.