oangle_sign_sub_right_eq_neg — Mathlib

English

For any x,y in a 2D real oriented space, the sign of the angle from x to x−y is the negation of the sign of the angle from x to y.

Русский

Для любых x,y знак угла от x к x−y является отрицанием знака угла от x к y.

LaTeX

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

Lean4

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

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