`BookProof.ChapterMeasurementLLN.outcomeIndicator_integral` (M : ℕ → Ω → Fin k) (a : Fin k) (hM : Measurable (M 0)) : ∫ ω, outcomeIndicator M a 0 ω ∂μ = (μ {ω

Initializing...

`BookProof.ChapterMeasurementLLN.outcomeIndicator_integral` (M : ℕ → Ω → Fin k) (a : Fin k) (hM : Measurable (M 0)) : ∫ ω, outcomeIndicator M a 0 ω ∂μ = (μ {ω | M 0 ω = a}).toReal · Prove2Me