mathlib

0d59511a - feat(topology/{continuous_function/bounded, metric_space/algebra}): new mixin classes (#8580)

feat(topology/{continuous_function/bounded, metric_space/algebra}): new mixin classes (#8580) This PR defines mixin classes `has_lipschitz_add` and `has_bounded_smul` which are designed to abstract algebraic properties of metric spaces shared by normed groups/fields/modules and by `ℝ≥0`. This permits the bounded continuous functions `α →ᵇ ℝ≥0` to be naturally a topological (ℝ≥0)-module, by a generalization of the proof previously written for normed groups/fields/modules. Frankly, these typeclasses are a bit ad hoc -- but it all seems to work!