mathlib

9b2b58d6 - feat(measure_theory/constructions): add the Borel isomorphism theorem. (#18864)

feat(measure_theory/constructions): add the Borel isomorphism theorem. (#18864) Add a file `measure_theory/constructions/borel_isomorphism.lean` with several versions of the Borel isomorphism theorem. Also add fairly small supporting lemmas in several other files. Most notable here is the addition of a type class for measurable_spaces whose sigma-algebras are generated by some countable set, and a theorem that such spaces admit measurable injections to the Cantor space. Co-authored-by: Felix-Weilacher <112423742+Felix-Weilacher@users.noreply.github.com>