oangle_sign_sub_left_swap — Mathlib

English

Swapping the two vectors after taking a certain left-right order preserves the sign of the angle up to negation.

Русский

Поменяв местами векторы, знак угла меняется на противоположный при выполнении соответствующих преобразований.

LaTeX

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

Lean4

/-- Subtracting the second vector passed to `oangle` from the first vector then swapping the
vectors does not change the sign of the angle. -/
@[simp]
theorem oangle_sign_sub_left_swap (x y : V) : (o.oangle (x - y) x).sign = (o.oangle x y).sign := by
  rw [oangle_sign_sub_left_eq_neg, o.oangle_rev y x, Real.Angle.sign_neg]

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