Theorem PMF.toMeasure_apply_eq_toOuterMeasure

Modification history

2025-06-23 17:18
Mathlib/Probability/ProbabilityMassFunction/Basic.lean
refactor(MeasureTheory/PMF): Removing `MasurableSet` hypotheses (#26230) …
Added PMF.toMeasure_apply_eq_toOuterMeasureView on Github →