Theorem disjoint_measurableAtom_of_notMem

Modification history

2025-08-07 07:24
Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean
feat: in a countable measurable space, every measure is s-finite (#27583) …
Added disjoint_measurableAtom_of_notMemView on Github →