oangle_sign_smul_sub_left — Mathlib

English

Subtracting a real multiple of the second vector from the first vector negates the angle sign.

Русский

Вычитание скалярного múltiplика второй векторы из первого меняет знак угла на противоположный.

LaTeX

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

Lean4

/-- Subtracting the first vector passed to `oangle` from a multiple of the second vector negates
the sign of the angle. -/
@[simp]
theorem oangle_sign_smul_sub_left (x y : V) (r : ℝ) : (o.oangle (r • y - x) y).sign = -(o.oangle x y).sign := by
  rw [← oangle_sign_neg_left, sub_eq_neg_add, oangle_sign_add_smul_left]

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