Commit 2023-07-22 18:41 8047de4dView 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.
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