mathlib3

e26a9e56 - feat(measure_theory/covering/besicovitch): the Besicovitch covering theorem (#9462)

feat(measure_theory/covering/besicovitch): the Besicovitch covering theorem (#9462) The Besicovitch covering theorem: in a nice metric space (e.g. real vector spaces), from any family of balls one can extract `N` subfamilies made of disjoint balls, covering all the centers of the balls in the family. The number `N` only depends on the metric space.