signedDist_triangle_right — Mathlib

English

For all v,p,q,r, signedDist v p q − signedDist v p r = signedDist v r q.

Русский

Для всех v,p,q,r: signedDist v p q − signedDist v p r = signedDist v r q.

LaTeX

$$signedDist v p q - signedDist v p r = signedDist v r q$$

Lean4

@[simp]
theorem signedDist_triangle_right : signedDist v p r - signedDist v q r = signedDist v p q := by
  rw [sub_eq_iff_eq_add, signedDist_triangle]
    -- Lemmas about offsetting the point arguments of `signedDist` (with `+ᵥ` or `-ᵥ`)

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