mathlib

11d5ff21 - feat(measure_theory/constructions/polish): a Polish Borel space is measurably equivalent to a subset of the reals (#18881)

feat(measure_theory/constructions/polish): a Polish Borel space is measurably equivalent to a subset of the reals (#18881) Co-authored-by: RemyDegenne <Remydegenne@gmail.com> Co-authored-by: Rémy Degenne <remydegenne@gmail.com>