measure_space): add instance `compact_space.is_finite_measure` (#15693)

Commit

3 years ago

feat(measure_theory/measure/measure_space): add instance `compact_space.is_finite_measure` (#15693)

Author

ocfnash

Parents