mathlib

bf6a0135 - chore(measure_theory/{constructions/borel_space,integral/lebesgue}): split (#19015)

chore(measure_theory/{constructions/borel_space,integral/lebesgue}): split (#19015) Remove dependence on ```text import analysis.complex.basic import analysis.normed_space.basic import topology.instances.add_circle import topology.metric_space.metrizable ``` from `measure_theory.constructions.borel_space` (in particular this gets rid of the `operator_norm` dependency, which is currently the big blocker) and `measure_theory.integral.lebesgue`.