English
Let V be a 2-dimensional real inner product space with an orientation o. For any x, y in V and any real r, the sign of the oriented angle from x to r·y is the product of the sign of r and the sign of the oriented angle from x to y.
Русский
Пусть V — двумерное вещественное вещественное пространство с ориентировкой o. Для любых векторов x, y ∈ V и любого действительного числа r знак ориентированного угла от x к r·y равен произведению знаков r и знака угла от x к y.
LaTeX
$$$\\forall x,y\\in V,\\ r\\in\\mathbb{R},\\ \\operatorname{sign}\\big(o.oangle(x, r\,y)\\big) = \\operatorname{sign}(r) \\cdot \\operatorname{sign}\\big(o.oangle(x,y)\\big)$$$
Lean4
/-- Multiplying the second vector passed to `oangle` by a real multiplies the sign of the angle by
the sign of the real. -/
@[simp]
theorem oangle_sign_smul_right (x y : V) (r : ℝ) : (o.oangle x (r • y)).sign = SignType.sign r * (o.oangle x y).sign :=
by rcases lt_trichotomy r 0 with (h | h | h) <;> simp [h]
