chore(measure_theory): a `continuous_map` is measurable (#9998)
chore(measure_theory): a `continuous_map` is measurable (#9998)

Also move the proof of `homeomorph.measurable` up and use it in the
definition of `homeomorph.to_measurable_equiv`.






leanprover-community/mathlib,leanprover-community/mathlib