Commit 2023-05-15 04:39 bf6a0135
View on Github →chore(measure_theory/{constructions/borel_space,integral/lebesgue}): split (#19015) Remove dependence on
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.