left_ne_right_of_oangle_sign_eq_neg_one

English

If the oriented angle ∡ p1 p2 p3 has sign -1, then p1 ≠ p3.

Русский

Если ориентированный угол ∡ p1 p2 p3 имеет знак −1, то p1 ≠ p3.

LaTeX

$$$ \forall p_1,p_2,p_3 : P,\ ( \angle p_1 p_2 p_3 ).\mathrm{sign} = -1 \rightarrow p_1 \neq p_3$$$

Lean4

/-- If the sign of the angle between three points is negative, the first and third points are not
equal. -/
theorem left_ne_right_of_oangle_sign_eq_neg_one {p₁ p₂ p₃ : P} (h : (∡ p₁ p₂ p₃).sign = -1) : p₁ ≠ p₃ :=
  left_ne_right_of_oangle_sign_ne_zero (h.symm ▸ by decide : (∡ p₁ p₂ p₃).sign ≠ 0)

Похожие утверждения