mathlib

6993e6f8 - feat(measure_theory/constructions/borel_space): decomposing the measure of a set into slices (#10096)

feat(measure_theory/constructions/borel_space): decomposing the measure of a set into slices (#10096) Also add the fact that `μ (to_measurable μ t ∩ s) = μ (t ∩ s)`, and useful variations around this fact.