Commit 2023-07-22 18:41 8047de4d

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!