Commit 2024-08-25 12:51 bd9ce04d

View on Github →

feat: The counting measure is nonzero (#16139) ... and other simple measure theory lemmas From LeanAPAP

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Count.lean

added theorem MeasureTheory.Measure.count_ne_zero''

added theorem MeasureTheory.Measure.count_univ

Modified Mathlib/MeasureTheory/Measure/Dirac.lean

added theorem MeasureTheory.Measure.dirac_ne_zero

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

modified theorem MeasureTheory.Measure.ae_smul_measure_eq

modified theorem MeasureTheory.Measure.ae_smul_measure_iff

added theorem MeasureTheory.Measure.sum_eq_zero