ratio_unique_of_nndist_ne_zero — Mathlib

English

If nndist x y ≠ 0 and hr : nndist(f x) (f y) = r · nndist x y, then r = ratio f.

Русский

Если nndist x y ≠ 0 и nndist(f x) (f y) = r · nndist x y, тогда r = ratio f.

LaTeX

$$nndist(f x) (f y) = r · nndist x y \Rightarrow r = ratio f$$

Lean4

/-- The `ratio` is equal to the distance ratio for any two points
with nonzero finite distance; `nndist` version -/
theorem ratio_unique_of_nndist_ne_zero {α β F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β]
    [DilationClass F α β] {f : F} {x y : α} {r : ℝ≥0} (hxy : nndist x y ≠ 0)
    (hr : nndist (f x) (f y) = r * nndist x y) : r = ratio f :=
  ratio_unique (by rwa [edist_nndist, ENNReal.coe_ne_zero]) (edist_ne_top x y)
    (by rw [edist_nndist, edist_nndist, hr, ENNReal.coe_mul])

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