mathlib

93f88091 - feat(topology/metric_space/dilation): Dilations on metric spaces (#14315)

feat(topology/metric_space/dilation): Dilations on metric spaces (#14315) We define `dilation α β` as the type of maps that satisfy `edist (f x) (f y) = r * edist x y` for all `x y`. Here `r : ℝ≥0`, so we do not exclude the degenerate case of dilations which collapse into constant maps. After this I will extend to `{linear, affine}_dilation_{equiv}`s and `{linear, affine}_isometry_{equiv}`s. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: JovanGerb <jovan.gerbscheid@gmail.com>