English
Let V be a 2-dimensional real inner product space with orientation o. For any x,y and real r, the sign of o.oangle(x, r·x + y) equals sign of r times sign of o.oangle(x, y).
Русский
Пусть V — двумерное пространство над ℝ с ориентированием o. Для любых векторов x,y и числа r: знак угла o.oangle(x, r·x + y) равен знаку r умноженному на знак угла o.oangle(x,y).
LaTeX
$$$\\forall x,y\\in V,\\ r\\in\\mathbb{R},\\ \\operatorname{sign}\\big(o.oangle(x, r\\,x+y)\\big) = \\operatorname{sign}(r) \\cdot \\operatorname{sign}\\big(o.oangle(x,y)\\big)$$$
Lean4
/-- Adding a multiple of the second vector passed to `oangle` to the first vector does not change
the sign of the angle. -/
@[simp]
theorem oangle_sign_add_smul_left (x y : V) (r : ℝ) : (o.oangle (x + r • y) y).sign = (o.oangle x y).sign := by
simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm x, oangle_sign_smul_add_right]
