English
Under the assumption that the signs of the oriented angles are equal, the equality of the unoriented angles is equivalent to the equality of the oriented angles.
Русский
При допущении равенства знаков ориентированных углов неориентированное равенство углов эквивалентно равенству ориентированных углов.
LaTeX
$$$\angle p_1 p_2 p_3 = \angle p_4 p_5 p_6 \;\iff\; (\measuredangle p_1 p_2 p_3).sign = (\measuredangle p_4 p_5 p_6).sign \Rightarrow \measuredangle p_1 p_2 p_3 = \measuredangle p_4 p_5 p_6$$$
Lean4
/-- If the signs of two nondegenerate oriented angles between points are equal, the oriented
angles are equal if and only if the unoriented angles are equal. -/
theorem angle_eq_iff_oangle_eq_of_sign_eq {p₁ p₂ p₃ p₄ p₅ p₆ : P} (hp₁ : p₁ ≠ p₂) (hp₃ : p₃ ≠ p₂) (hp₄ : p₄ ≠ p₅)
(hp₆ : p₆ ≠ p₅) (hs : (∡ p₁ p₂ p₃).sign = (∡ p₄ p₅ p₆).sign) : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆ ↔ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ :=
o.angle_eq_iff_oangle_eq_of_sign_eq (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₃) (vsub_ne_zero.2 hp₄)
(vsub_ne_zero.2 hp₆) hs
