Theorem MeasureTheory.Measure.ofMultiset_apply_singleton_of_notMem

Modification history

2026-10-05 07:41
Mathlib/Probability/Distributions/Uniform.lean
refactor(Probability/Distributions/Uniform): change uniformOfFinset and ofMultiset from PMF to Measure (#42909) …
Added MeasureTheory.Measure.ofMultiset_apply_singleton_of_notMemView on Github →