`BookProof.ChapterAtomicDecomposition.probability_measure_five_types` (mu : Measure X) [IsProbabilityMeasure mu] : (continuousPart mu = 0 ∧ (atoms mu).Finite ∧ (atoms mu).Nonempty)
ProvedBookProof.ChapterAtomicDecomposition.probability_measure_five_typestheoremstimepiece
Prove the following Lean 4 theorem from ChapterAtomicDecomposition.
BookProof.ChapterAtomicDecomposition.probability_measure_five_types (mu : Measure X) [IsProbabilityMeasure mu] : (continuousPart mu = 0 ∧ (atoms mu).Finite ∧ (atoms mu).Nonempty) ∨ (continuousPart mu = 0 ∧ (atoms mu).Infinite) ∨ (continuousPart mu ≠ 0 ∧ atoms mu = ∅) ∨ (continuousPart mu ≠ 0 ∧ (atoms mu).Finite ∧ (atoms mu).Nonempty) ∨ (continuousPart mu ≠ 0 ∧ (atoms mu).Infinite)
Formalization note: Lean 4 identifier BookProof.ChapterAtomicDecomposition.probability_measure_five_types.
Preamble
-- Generated from ChapterAtomicDecomposition.lean — theorem BookProof.ChapterAtomicDecomposition.probability_measure_five_types
import Mathlib
import Definitions.Def_ChapterAtomicDecomposition
open BookProof.ChapterAtomicDecomposition
open MeasureTheory
variable {X : Type*} [MeasurableSpace X] [MeasurableSingletonClass X]Formal statement
theorem BookProof.ChapterAtomicDecomposition.probability_measure_five_types (mu : Measure X) [IsProbabilityMeasure mu] :
(continuousPart mu = 0 ∧ (atoms mu).Finite ∧ (atoms mu).Nonempty) ∨
(continuousPart mu = 0 ∧ (atoms mu).Infinite) ∨
(continuousPart mu ≠ 0 ∧ atoms mu = ∅) ∨
(continuousPart mu ≠ 0 ∧ (atoms mu).Finite ∧ (atoms mu).Nonempty) ∨
(continuousPart mu ≠ 0 ∧ (atoms mu).Infinite) := by sorry