Commit 2025-08-07 07:24 cde6b588

View on Github →

feat: in a countable measurable space, every measure is s-finite (#27583) Also add API lemmas about measurableAtom. The instance is placed in the WithDensity file, because that's where we have the instance SFinite (c • μ) that I use in the proof.

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean

added theorem disjoint_measurableAtom_of_notMem

added theorem measurableAtom_eq_of_mem

added theorem measurableAtom_subset_of_mem

Modified Mathlib/MeasureTheory/Measure/Dirac.lean

added theorem MeasureTheory.Measure.exists_sum_smul_dirac

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.ext_of_measurableAtoms

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean