mathlib3

8181fe89 - feat(measure_theory/covering/besicovitch): covering a set by balls with controlled measure (#11035)

feat(measure_theory/covering/besicovitch): covering a set by balls with controlled measure (#11035) We show that, in a real vector space, any set `s` can be covered by balls whose measures add up to at most `μ s + ε`, as a consequence of the Besicovitch covering theorem. Co-authored-by: Johan Commelin <johan@commelin.net>