Theorem MeasureTheory.Measure.sum_of_isEmpty

Modification history

2024-06-16 19:40
Mathlib/MeasureTheory/Measure/MeasureSpace.lean
chore: Golf `Finset.prod_ite_of_true` (#13726) …
Added MeasureTheory.Measure.sum_of_isEmptyView on Github →