mathlib

159766e9 - chore(topology/metric_space/basic): rename `uniform_continuous_dist'` (#3145)

chore(topology/metric_space/basic): rename `uniform_continuous_dist'` (#3145) * rename `uniform_continuous_dist'` to `uniform_continuous_dist`; * rename `uniform_continuous_dist` to `uniform_continuous.dist`; * add `uniform_continuous.nndist`.