toDilationEquiv_ratio — Mathlib

English

If e is an isometry from X to Y, then the associated dilation-equivalence has ratio equal to 1.

Русский

Если e — изометрия между метрическими пространствами X и Y, то соответствующая дилатационная эквивалентность имеет коэффициент равный 1.

LaTeX

$$$ \mathrm{ratio}(e^{\mathrm{toDilationEquiv}}) = 1 $$$

Lean4

@[simp]
theorem _root_.IsometryEquiv.toDilationEquiv_ratio (e : X ≃ᵢ Y) : ratio e.toDilationEquiv = 1 := by
  rw [← ratio_toDilation, IsometryEquiv.toDilationEquiv_toDilation, Isometry.toDilation_ratio]

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