Fixed short scale implies global nonexpansiveness

This module formalizes the line-segment subdivision argument from the preliminaries of paper1.

theorem ScottishBook155.dist_image_le_of_subdivision {M : Type u_1} {N : Type u_2} [NormedAddCommGroup M] [NormedSpace ℝ M] [PseudoMetricSpace N] {r : ℝ} {V : M → N} (hshort : PreservesUpTo r V) {x y : M} (n : ℕ) (hn : 0 < n) (hstep : dist x y / ↑n ≤ r) : dist (V x) (V y) ≤ dist x y

theorem ScottishBook155.preservesUpTo_nonexpansive {M : Type u_1} {N : Type u_2} [NormedAddCommGroup M] [NormedSpace ℝ M] [PseudoMetricSpace N] {r : ℝ} (hr : 0 < r) {V : M → N} (hshort : PreservesUpTo r V) (x y : M) : dist (V x) (V y) ≤ dist x y