mathlib3

2675b5c3 - feat(measure_theory/constructions/polish): injective images of Borel sets in Polish spaces are Borel (#12448)

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