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

leanprover-community/mathlib,leanprover-community/mathlib