signedDist_right_congr — Mathlib

English

If ⟪v, q −ᵥ r⟫ = 0 then signedDist v p q = signedDist v p r for all p.

Русский

Если ⟪v, q −ᵥ r⟫ = 0, то для всех p выполняется signedDist v p q = signedDist v p r.

LaTeX

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

Lean4

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

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