Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes