Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-24 14:25 7fba1afa

View on Github →

fix(analysis/metric_space): remove superfluous typeclass assumptions

Estimated changes

Modified analysis/metric_space.lean

modified theorem continuous_of_metric

modified theorem tendsto_dist

modified theorem tendsto_nhds_of_metric

modified theorem uniform_continuous_of_metric

modified theorem uniform_embedding_of_metric