Theorem MeasureTheory.setIntegral_diff

Modification history

2026-03-05 01:06
Mathlib/MeasureTheory/Integral/Bochner/Set.lean
feat(Integral.Bochner.Set): add `tendsto_setIntegral_of_monotone₀` (#34025) …
Added MeasureTheory.setIntegral_diffView on Github →