Commit 2022-04-07 18:41 9d786ce7
View on Github →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.