mathlib

dc589c89 - fix(topology/bornology): turn `bounded_space` into a `mixin` (#13615)

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`.