mathlib

771f2b7b - 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 <urkud@urkud.name>