Commit 2022-04-27 15:34 dc589c89
View on Github →fix(topology/bornology): turn bounded_space into a mixin (#13615)
Otherwise, we would need bounded_pseudo_metric_space,
bounded_metric_space etc.
Also add set.finite.is_bounded, bornology.is_bounded.all, and
bornology.is_bounded_univ.