English
If two pairs of distinct points lie on the same line and the corresponding vectors are on the same ray, the oriented angles at a fixed point p4 have the same sign.
Русский
Если две пары точек лежат на одной прямой и соответствующие векторы направлены в один луч, знаки углов около p4 совпадают.
LaTeX
$$$Collinear_\mathbb{R}({p_1,p_2,p_3,p_4}) \Rightarrow (\angle p_1 p_4 p_2).sign = (\angle p_3 p_4 p_4).sign$$$
Lean4
/-- Given three points in weak order on the same line, with the first not equal to the second,
and a fourth point, the angles at the fourth point between the first and second or first and
third points have the same sign. -/
theorem _root_.Wbtw.oangle_sign_eq_of_ne_left {p₁ p₂ p₃ : P} (p₄ : P) (h : Wbtw ℝ p₁ p₂ p₃) (hne : p₁ ≠ p₂) :
(∡ p₁ p₄ p₂).sign = (∡ p₁ p₄ p₃).sign :=
haveI hc : Collinear ℝ ({ p₁, p₂, p₁, p₃ } : Set P) := by simpa [Set.insert_comm p₂] using h.collinear
hc.oangle_sign_of_sameRay_vsub _ hne (h.left_ne_right_of_ne_left hne.symm) h.sameRay_vsub_left
