mathlib3

d212f3eb - feat(measure_theory/measure): new class is_finite_measure_on_compacts (#10827)

feat(measure_theory/measure): new class is_finite_measure_on_compacts (#10827) We have currently four independent type classes guaranteeing that a measure of compact sets is finite: `is_locally_finite_measure`, `is_regular_measure`, `is_haar_measure` and `is_add_haar_measure`. Instead of repeting lemmas for all these classes, we introduce a new typeclass saying that a measure is finite on compact sets.