mathlib3

6b766f92 - feat(measure_theory/measure/measure_space): In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts. (#15492)

feat(measure_theory/measure/measure_space): In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts. (#15492) Main addition of this PR: In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts. Also in this PR: A disjoint union whose measure is finite has at most finitely many parts of measure greater than any positive constant. Co-authored-by: kkytola <“kalle.kytola@aalto.fi”>