feat(topology/metric_space/basic): union of balls `ball x n`, `n : ℕ` (#8792)
feat(topology/metric_space/basic): union of balls `ball x n`, `n : ℕ` (#8792)





leanprover-community/mathlib,leanprover-community/mathlib