Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-23 08:40 159766e9

View on Github →

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.

Estimated changes

Modified src/topology/metric_space/basic.lean

added theorem uniform_continuous.dist

added theorem uniform_continuous.nndist

deleted theorem uniform_continuous_dist'

modified theorem uniform_continuous_dist

Modified src/topology/metric_space/completion.lean