I did finally write up that covering argument in Haskell, the core of it is

vitali :: [Ball] -> [Ball]
vitali [] = []
vitali balls =
let b = maximumBy (compare on radius) balls
newBalls = filter (not . intersects b) balls
in b : vitali newBalls

(the significance is that you can show that the new collection of balls here is disjoint and has total volume ≥ 1/3ᵈ times the total volume of the original collection.)

A Mastodon instance for maths people. The kind of people who make $\pi z^2 \times a$ jokes.

Use $ and $ for inline LaTeX, and $ and $ for display mode.