Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-02-19 10:38 3ef7c7df

View on Github →

fix(analysis/metric_space): remove unnecessary topological_space assumption from tendsto_dist

Estimated changes

modified theorem tendsto_dist