Commit 2026-02-05 00:24 8247c9ec

View on Github →

feat(MeasureTheory): characterise when a measure is supported on a finset (#34374)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Dirac.lean

added theorem MeasureTheory.Measure.ae_eq_or_eq_iff_eq_dirac_add_dirac

added theorem MeasureTheory.Measure.ae_eq_or_eq_iff_map_eq_dirac_add_dirac

added theorem MeasureTheory.Measure.ae_mem_finset_iff

added theorem MeasureTheory.Measure.ae_mem_finset_iff_map_eq_sum_dirac

modified theorem MeasureTheory.ae_dirac_iff

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

modified theorem MeasureTheory.ae_add_measure_iff

added theorem MeasureTheory.ae_finsetSum_measure_iff