Theorem BoundedContinuousFunction.apply_le_edist_zero

Modification history

2026-05-29 07:38
Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
feat(MeasureTheory/Function): ae convergence implies convergence in distribution (#39517) …
Added BoundedContinuousFunction.apply_le_edist_zeroView on Github →