English
For any dilation f and points x,y, dist(f x, f y) = ratio(f) · dist(x,y).
Русский
Для дилатации f и точек x,y расстояние после применения дилатации равно ratio(f) умножить на расстояние до применения: dist(f x, f y) = ratio(f) · dist(x,y).
LaTeX
$$dist(f x, f y) = ratio f \cdot dist x y$$
Lean4
@[simp]
theorem dist_eq {α β F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β]
(f : F) (x y : α) : dist (f x) (f y) = ratio f * dist x y := by simp only [dist_nndist, nndist_eq, NNReal.coe_mul]