toDilation_ratio — Mathlib

English

For an isometry f with toDilation structure, the associated ratio equals 1.

Русский

Для изометрии f с конструкцией toDilation соответствующее ratio равно 1.

LaTeX

$$ratio (Isometry.toDilation f hf) = 1$$

Lean4

@[simp]
theorem _root_.Isometry.toDilation_ratio {f : α → β} {hf : Isometry f} : ratio hf.toDilation = 1 :=
  by
  by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ⊤
  · exact ratio_of_trivial hf.toDilation h
  · push_neg at h
    obtain ⟨x, y, h₁, h₂⟩ := h
    exact ratio_unique h₁ h₂ (by simp [hf x y]) |>.symm

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