edist_eq — Mathlib

English

If f is an isometry, then the associated dilation has ratio 1.

Русский

Если f является изометрией, связанная дилатация имеет ratio равный 1.

LaTeX

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

Lean4

@[simp]
theorem edist_eq [DilationClass F α β] (f : F) (x y : α) : edist (f x) (f y) = ratio f * edist x y :=
  by
  rw [ratio]; split_ifs with key
  · rcases DilationClass.edist_eq' f with ⟨r, hne, hr⟩
    replace hr := hr x y
    rcases key x y with h | h
    · simp only [hr, h, mul_zero]
    · simp [hr, h, hne]
  exact (DilationClass.edist_eq' f).choose_spec.2 x y

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