Theorem MeasureTheory.tendsto_setIntegral_of_monotone₀

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.tendsto_setIntegral_of_monotone₀View on Github →