2022-11-26 00:19
src/measure_theory/measure/probability_measure.lean
feat(measure_theory/measure/probability_measure): Add a bit of simple API to probability_measure. (#17610) …
Added measure_theory.probability_measure.nonempty_of_probability_measure