neg_vsub_eq_vsub_rev — Mathlib

English

The negation of vsub equals the reversed vsub: -(p1 -ᵥ p2) = p2 -ᵥ p1.

Русский

Отрицание VSub равно обратному VSub: -(p1 -ᵥ p2) = p2 -ᵥ p1.

LaTeX

$$$-\vsub(p_1,p_2) = vsub(p_2,p_1)$$$

Lean4

/-- Subtracting two points in the reverse order produces the negation
of subtracting them. -/
@[simp]
theorem neg_vsub_eq_vsub_rev (p₁ p₂ : P) : -(p₁ -ᵥ p₂) = p₂ -ᵥ p₁ :=
  by
  refine neg_eq_of_add_eq_zero_right (vadd_right_cancel p₁ ?_)
  rw [vsub_add_vsub_cancel, vsub_self]

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