Theorem PMF.toMeasure_apply_eq_tsum

Modification history

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