Commit 2022-03-07 10:15 2675b5c3

feat(measure_theory/constructions/polish): injective images of Borel sets in Polish spaces are Borel (#12448) We prove several fundamental results on the Borel sigma-algebra in Polish spaces, notably:

• Lusin separation theorem: disjoint analytic sets can be separated via Borel sets
• Lusin-Souslin theorem: a continuous injective image of a Borel set in a Polish space is Borel
• An injective measurable map on a Polish space is a measurable embedding, i.e., it maps measurable sets to measurable sets