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.
\) for inline LaTeX, and
\] for display mode.