Theorem MeasureTheory.aecover_closedBall

Modification history

2024-02-22 17:05
Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
feat: extend convergence of integrals against peak functions to noncompact settings (#10829) …
Added MeasureTheory.aecover_closedBallView on Github →