oangle_sign_neg_left — Mathlib

English

Negating the first vector twice leaves the sign unchanged: (o.oangle (−(−x)) y).sign = (o.oangle x y).sign.

Русский

Двойное отрицание первого вектора не меняет знак: o.oangle(−(−x), y).sign = o.oangle(x,y).sign.

LaTeX

$$$ (o.oangle (-(-x)) y).sign = (o.oangle x y).sign $$$

Lean4

/-- Negating the first vector passed to `oangle` negates the sign of the angle. -/
@[simp]
theorem oangle_sign_neg_left (x y : V) : (o.oangle (-x) y).sign = -(o.oangle x y).sign :=
  by
  by_cases hx : x = 0; · simp [hx]
  by_cases hy : y = 0; · simp [hy]
  rw [o.oangle_neg_left hx hy, Real.Angle.sign_add_pi]

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