`BookProof.ChapterAtomicDecomposition.measurableSet_atoms` (mu : Measure X) [SFinite mu] : MeasurableSet (atoms mu)
ProvedBookProof.ChapterAtomicDecomposition.measurableSet_atomstheoremstimepiece
Prove the following Lean 4 theorem from ChapterAtomicDecomposition.
BookProof.ChapterAtomicDecomposition.measurableSet_atoms (mu : Measure X) [SFinite mu] : MeasurableSet (atoms mu)
Formalization note: Lean 4 identifier BookProof.ChapterAtomicDecomposition.measurableSet_atoms.
Preamble
-- Generated from ChapterAtomicDecomposition.lean — theorem BookProof.ChapterAtomicDecomposition.measurableSet_atoms
import Mathlib
import Definitions.Def_ChapterAtomicDecomposition
open BookProof.ChapterAtomicDecomposition
open MeasureTheory
variable {X : Type*} [MeasurableSpace X] [MeasurableSingletonClass X]Formal statement
theorem BookProof.ChapterAtomicDecomposition.measurableSet_atoms (mu : Measure X) [SFinite mu] : MeasurableSet (atoms mu) := by sorry