English
If dist x y ≠ 0 and hr : dist(f x) (f y) = r · dist x y, then r = ratio f.
Русский
Если dist x y ≠ 0 и dist(f x) (f y) = r · dist x y, тогда r = ratio f.
LaTeX
$$dist(f x) (f y) = r · dist x y \Rightarrow r = ratio f$$
Lean4
/-- The `ratio` is equal to the distance ratio for any two points
with nonzero finite distance; `dist` version -/
theorem ratio_unique_of_dist_ne_zero {α β} {F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β]
[DilationClass F α β] {f : F} {x y : α} {r : ℝ≥0} (hxy : dist x y ≠ 0) (hr : dist (f x) (f y) = r * dist x y) :
r = ratio f :=
ratio_unique_of_nndist_ne_zero (NNReal.coe_ne_zero.1 hxy) <|
NNReal.eq <| by rw [coe_nndist, hr, NNReal.coe_mul, coe_nndist]