Commit 2024-10-13 10:51 56401289
View on Github →chore: generalize strong law of large numbers from MeasureSpace to MeasurableSpace (#17692)
See discussion at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60MeasureSpace.60.20vs.20.60Measure.60.20in.20.60ProbabilityTheory.2F.60/near/476526619