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