Theorem MeasureTheory.AddContent.onIocAux_empty

Modification history

2026-01-27 08:06
Mathlib/MeasureTheory/Measure/AddContent.lean
feat: additive content on open-closed intervals, mapping `(u, v]` to `f v - f u` (#34462) …
Added MeasureTheory.AddContent.onIocAux_emptyView on Github →