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