# Commit 2023-07-22 18:41 8047de4d

View on Github →feat(topology/metric_space/basic): decomposition of a "sphere" hypercube (#18875)
The main result here is `sphere x r = (⋃ i : β, function.eval i ⁻¹' sphere (x i) r) ∩ closed_ball x r`

, which attempts to express that you can form the surface of a cube by taking the union of the faces in each axis.
The `prod`

result, `sphere (x, y) r = sphere x r ×ˢ closed_ball y r ∪ closed_ball x r ×ˢ sphere y r`

, is a little easier to follow.
I can imagine these being useful if we wanted to prove that the surface area of a "sphere" in `fin 3 -> R`

was `24*r*r`

!