Theorem MeasureTheory.ae_le_const_iff_forall_gt_measure_zero

Modification history

2025-01-05 13:11
Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean
feat: a conditional kernel is almost everywhere a probability measure (#20430)
Added MeasureTheory.ae_le_const_iff_forall_gt_measure_zeroView on Github →