oangle_sign_sub_left_eq_neg — Mathlib

English

Subtracting the first vector from the second in an oriented angle flips the sign.

Русский

Вычитание первого вектора из второго в отношении ориентации разворачивает знак.

LaTeX

$$$\\forall x,y\\in V,\\ o.oangle(y - x, y).sign = -\\big(o.oangle(x,y).sign\\big)$$$

Lean4

/-- Subtracting the first vector passed to `oangle` from the second vector negates the sign of
the angle. -/
theorem oangle_sign_sub_left_eq_neg (x y : V) : (o.oangle (y - x) y).sign = -(o.oangle x y).sign := by
  rw [← o.oangle_sign_smul_sub_left x y 1, one_smul]

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