mathlib3

b0349aa9 - 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`.