signedDist_left_congr — Mathlib

English

If ⟪v, p −ᵥ q⟫ = 0, then signedDist v p = signedDist v q as functions of (p,q).

Русский

Если ⟪v, p −ᵥ q⟫ = 0, то signedDist v p = signedDist v q как функции от (p,q).

LaTeX

$$⟨v, p -ᵥ q⟩ = 0 ⇒ signedDist(v) p = signedDist(v) q$$

Lean4

theorem signedDist_left_congr (h : ⟪v, p -ᵥ q⟫ = 0) : signedDist v p = signedDist v q :=
  by
  ext r
  simpa [NormedSpace.normalize, real_inner_smul_left, h] using signedDist_vadd_left v (p -ᵥ q) q r

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