mathlib

13cd192e - feat(measure_theory/measure_space): added sub for measure_theory.measure (#4639)

feat(measure_theory/measure_space): added sub for measure_theory.measure (#4639) This definition is useful for proving the Lebesgue-Radon-Nikodym theorem for non-negative measures. Co-authored-by: mzinkevi <41597957+mzinkevi@users.noreply.github.com>