probability_measure): Add a bit of simple API to probability_measure. (#17610)

Commit

3 years ago

feat(measure_theory/measure/probability_measure): Add a bit of simple API to probability_measure. (#17610) Add a bit of simple API to `probability_measure` and `finite_measure`.

Author

kkytola

Parents

44e2d1e4

mathlib 0f74a7a1 - feat(measure_theory/measure/probability_measure): Add a bit of simple API to probability_measure. (#17610)

mathlib
0f74a7a1 - feat(measure_theory/measure/probability_measure): Add a bit of simple API to probability_measure. (#17610)