English
Multiplying the first vector by a real r scales the sign of the oriented angle by Sign(r): (o.oangle (r•x) y).sign = Sign(r) · (o.oangle x y).sign.
Русский
Умножение первого вектора на вещественное число r масштабирует знак ориентированного угла: (o.oangle (r·x) y).sign = Sign(r) · (o.oangle x y).sign.
LaTeX
$$$ (o.oangle (r \cdot x) y).sign = \operatorname{sign}(r) \cdot (o.oangle x y).sign $$$
Lean4
/-- The oriented angle between two vectors equals minus the unoriented angle if the sign is
negative. -/
theorem oangle_eq_neg_angle_of_sign_eq_neg_one {x y : V} (h : (o.oangle x y).sign = -1) :
o.oangle x y = -InnerProductGeometry.angle x y :=
by
by_cases hx : x = 0; · simp [hx] at h
by_cases hy : y = 0; · simp [hy] at h
refine (o.oangle_eq_angle_or_eq_neg_angle hx hy).resolve_left ?_
intro hxy
rw [hxy, ← SignType.neg_iff, ← not_le] at h
exact
h
(Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi (InnerProductGeometry.angle_nonneg _ _)
(InnerProductGeometry.angle_le_pi _ _))
