Theorem measure_theory.measure.countable_meas_pos_of_disjoint_of_meas_Union_ne_top
Modification history
2022-12-04 09:54
src/measure_theory/measure/measure_space.lean
feat(measure_theory/measure/measure_space): In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts. (#15492) …
Added measure_theory.measure.countable_meas_pos_of_disjoint_of_meas_Union_ne_topView on Github →