`BookProof.ChapterG3.integral_eventProj` [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (A : Set X) (hA : MeasurableSet A) : ∫ x, eventProj A x ∂μ = (μ A).toReal

Initializing...

`BookProof.ChapterG3.integral_eventProj` [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (A : Set X) (hA : MeasurableSet A) : ∫ x, eventProj A x ∂μ = (μ A).toReal · Prove2Me