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