chore(topology/metric_space/basic): add `metric_space.replace_bornology` (#14638)
chore(topology/metric_space/basic): add `metric_space.replace_bornology` (#14638)

We have the `pseudo_metric_space` version from #13927, but not the `metric_space` version.





Co-authored-by: Yury G. Kudryashov <2c59405d0ec2e119a1c3d2318bdb4a6ce50051ae@urkud.name>

leanprover-community/mathlib,leanprover-community/mathlib