Theorem MeasureTheory.tendsto_integral_thickenedIndicator_of_isClosed

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.tendsto_integral_thickenedIndicator_of_isClosedView on Github →