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