Theorem MeasureTheory.exists_accPt_of_noAtoms

Modification history

2026-06-22 10:16
Mathlib/MeasureTheory/Measure/Typeclasses/NullSingletonClass.lean
refactor(MeasureTheory/Measure/Typeclasses/NoAtoms): rename `NoAtoms` to `NullSingletonClass` (#40809) …
Deleted MeasureTheory.exists_accPt_of_noAtomsView on Github →
2026-01-29 13:31
Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean
feat(MeasureTheory/Measure/TypeClass/NoAtoms): add `exists_accPt_of_noAtoms` (#32851) …
Added MeasureTheory.exists_accPt_of_noAtomsView on Github →