Commit 2021-08-18 18:52 0d59511a

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!