def ProjectionTheory.HasHausdorffSpacing {α : Type u_1} [PseudoMetricSpace α] (X : Finset α) (R : ℝ) : Prop

Definition (Hausdorff spacing). A finite set X in a (pseudo)metric space has Hausdorff spacing at scale R if there is a uniform constant C > 0 such that for every exponent β ∈ [0, 1] and every centre c, the number of points of X within distance R^β of c satisfies $N_{R^\beta}(X) \le C\,|X|^\beta$.