Theorem MeasureTheory.integrable_thickenedIndicator

Modification history

2025-10-28 16:45
Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean
feat: Lipschitz function criterion for weak convergence of probability measures (#30742) …
Added MeasureTheory.integrable_thickenedIndicatorView on Github →