mathlib

84a1bd6a - refactor(topology/metric_space/basic): add `pseudo_metric_space.to_bornology'` (#13927)

refactor(topology/metric_space/basic): add `pseudo_metric_space.to_bornology'` (#13927) * add `pseudo_metric_space.to_bornology'` and `pseudo_metric_space.replace_bornology`; * add `metric.is_bounded_iff` and a few similar lemmas; * fix instances for `subtype`, `prod`, `pi`, and `pi_Lp` to use the correct bornology`; * add `lipschitz_with.to_locally_bounded_map` and `lipschitz_with.comap_cobounded_le`; * add `antilipschitz_with.tendsto_cobounded`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>