English
If for some x,y with suitable nondegeneracy we have edist(f x, f y) = r · edist(x,y), then r = ratio f.
Русский
Если для некоторых x,y с допустимым расстоянием выполнено edist(f x, f y) = r · edist(x,y), тогда r равно ratio f.
LaTeX
$$edist(f x, f y) = r · edist(x,y) \Rightarrow r = ratio f$$
Lean4
/-- The `ratio` is equal to the distance ratio for any two points with nonzero finite distance.
`dist` and `nndist` versions below -/
theorem ratio_unique [DilationClass F α β] {f : F} {x y : α} {r : ℝ≥0} (h₀ : edist x y ≠ 0) (htop : edist x y ≠ ⊤)
(hr : edist (f x) (f y) = r * edist x y) : r = ratio f := by
simpa only [hr, ENNReal.mul_left_inj h₀ htop, ENNReal.coe_inj] using edist_eq f x y