oangle_sign_smul_sub_right — Mathlib

English

For any x,y and r in a 2D real inner product space with orientation o, the sign of o.oangle(x, x − y) is the negation of the sign of o.oangle(x,y).

Русский

Для любых x,y и r знак o.oangle(x, x − y) равен противоположному знаку o.oangle(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 a multiple of the first vector negates
the sign of the angle. -/
@[simp]
theorem oangle_sign_smul_sub_right (x y : V) (r : ℝ) : (o.oangle x (r • x - y)).sign = -(o.oangle x y).sign := by
  rw [← oangle_sign_neg_right, sub_eq_add_neg, oangle_sign_smul_add_right]

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