mathlib
8572c6b0 - feat(topology): prove continuity of nndist and edist; `ball a r` is a metric space
