Is every set of diameter $1$ in ${\mathbb{R}}^n$ the union of at most $n+1$ sets of diameter $<1$?

AMS 52 · test (literature)

theorem erdos_505.test_dim_one
    (S : Set (EuclideanSpace ℝ (Fin 1)))
    (hS : Bornology.IsBounded S) (hd : 0 < diam S) :
    ∃ (F : Fin 2 → Set (EuclideanSpace ℝ (Fin 1))),
      S ⊆ ⋃ i, F i ∧ ∀ i, diam (F i) < diam S