ratio_unique_of_dist_ne_zero — Mathlib

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]

Похожие утверждения