ratio_unique — Mathlib

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

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