Theorem MeasureTheory.Measure.IsAtom.not_isAtom_iff_exists

Modification history

2026-11-10 19:03
Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean
feat(MeasureTheory): add `IsAtom` and `NoAtoms` (#45666) …
Added MeasureTheory.Measure.IsAtom.not_isAtom_iff_existsView on Github →