mathlib

ebccce9b - feat(measure_theory/covering/besicovitch): the measurable Besicovitch covering theorem (#9576)

feat(measure_theory/covering/besicovitch): the measurable Besicovitch covering theorem (#9576) The measurable Besicovitch theorem ensures that, in nice metric spaces, if at every point one considers a class of balls of arbitrarily small radii, called admissible balls, then one can cover almost all the space by a family of disjoint admissible balls. It is deduced from the topological Besicovitch theorem.