signedDist_congr — Mathlib

English

For any w ∈ V and p,q ∈ P, (signedDist v) evaluated at (p) and (q) is invariant under translating both arguments by w: signedDist v (w + p) (w + q) = signedDist v p q.

Русский

Для любого w ∈ V и p,q ∈ P выполняется: signedDist v (w + p) (w + q) = signedDist v p q.

LaTeX

$$$signedDist\ v\ (w+\!\!p)\ (w+\!\!q) = signedDist\ v\ p\ q$$$

Lean4

theorem signedDist_congr (h : ∃ r > (0 : ℝ), r • v = w) : signedDist (P := P) v = signedDist w :=
  by
  obtain ⟨r, _, _⟩ := h
  ext p q
  simpa [*] using (signedDist_smul v p q r).symm

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