mathlib

a30c39e0 - feat(measure_theory/borel_space): a compact set has finite measure (#5628)