measure_space): add some `null_measurable_set` lemmas (#14293)

Commit

4 years ago

feat(measure_theory/measure/measure_space): add some `null_measurable_set` lemmas (#14293) Add `measure_bUnion₀`, `measure_sUnion₀`, and `measure_bUnion_finset₀`.

Author

urkud

Parents

726b9ce7

mathlib ac006036 - feat(measure_theory/measure/measure_space): add some `null_measurable_set` lemmas (#14293)

mathlib
ac006036 - feat(measure_theory/measure/measure_space): add some `null_measurable_set` lemmas (#14293)