mathlib
f4d72050 - chore(measure_theory/*): rename `probability_measure` and `finite_measure` (#8831)

Commit
4 years ago
chore(measure_theory/*): rename `probability_measure` and `finite_measure` (#8831) Renamed to `is_probability_measure` and `is_finite_measure`, respectively. Also, `locally_finite_measure` becomes `is_locally_finite_measure`. See https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238337.20Weak.20convergence
Author
Parents
Loading