Commit 2022-04-07 18:41 9d786ce7

feat(topology/metric/basic): construct a bornology from metric axioms and add it to the pseudo metric structure (#12078) Every metric structure naturally gives rise to a bornology where the bounded sets are precisely the metric bounded sets. The eventual goal will be to replace the existing metric.bounded with one defined in terms of the bornology, so we need to construct the bornology first, as we do here.