Commit 2021-10-02 09:30 e26a9e56View 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.