`BookProof.ChapterMeasureAtomicDiffuse.restrict_atomSet_add_restrict_compl` [IsFiniteMeasure mu] : mu.restrict (atomSet mu) + mu.restrict (atomSet mu)ᶜ = mu
ProvedBookProof.ChapterMeasureAtomicDiffuse.restrict_atomSet_add_restrict_compltheoremstimepiece
Prove the following Lean 4 theorem from ChapterMeasureAtomicDiffuse.
BookProof.ChapterMeasureAtomicDiffuse.restrict_atomSet_add_restrict_compl [IsFiniteMeasure mu] : mu.restrict (atomSet mu) + mu.restrict (atomSet mu)ᶜ = mu
Formalization note: Lean 4 identifier BookProof.ChapterMeasureAtomicDiffuse.restrict_atomSet_add_restrict_compl.
Preamble
-- Generated from ChapterMeasureAtomicDiffuse.lean — theorem BookProof.ChapterMeasureAtomicDiffuse.restrict_atomSet_add_restrict_compl
import Mathlib
import Definitions.Def_ChapterMeasureAtomicDiffuse
open BookProof.ChapterMeasureAtomicDiffuse
noncomputable section
open MeasureTheory Complex
variable {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] (mu : Measure α)Formal statement
theorem BookProof.ChapterMeasureAtomicDiffuse.restrict_atomSet_add_restrict_compl [IsFiniteMeasure mu] :
mu.restrict (atomSet mu) + mu.restrict (atomSet mu)ᶜ = mu := by sorry