Commit 2021-10-02 09:30 e26a9e56
View on Github →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.