mathlib

8047de4d - feat(topology/metric_space/basic): decomposition of a "sphere" hypercube (#18875)

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`! Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>