English
For any vectors x,y and reals r1,r2, the sign of the angle between (r1 x + r2 y) and y is the sign of r1 times the sign of the angle between x and y.
Русский
Для любых x,y и чисел r1,r2 знак угла между (r1 x + r2 y) и y равен знаку r1, умноженному на знак угла между x и y.
LaTeX
$$$\\forall x,y\\in V,\\ r_1,r_2\\in\\mathbb{R},\\ (o.oangle(r_1 x + r_2 y, y)).sign = \\operatorname{sign}(r_1) \\cdot (o.oangle(x,y)).sign$$$
Lean4
/-- The sign of the angle between a linear combination of two vectors and the second vector is
the sign of the factor by which the first vector is multiplied in that combination multiplied by
the sign of the angle between the two vectors. -/
theorem oangle_sign_smul_add_smul_left (x y : V) (r₁ r₂ : ℝ) :
(o.oangle (r₁ • x + r₂ • y) y).sign = SignType.sign r₁ * (o.oangle x y).sign := by
simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm (r₁ • x), oangle_sign_smul_add_smul_right, mul_neg]
