right_ne_of_oangle_sign_eq_one — Mathlib

English

Let p1, p2, p3 be points in a 2D oriented Euclidean setting. If the oriented angle ∡ p1 p2 p3 has positive sign, then p3 ≠ p2.

Русский

Пусть p1, p2, p3 — точки в двумерной ориентированной Евклидовой геометрии. Если ориентированный угол ∡ p1 p2 p3 имеет положительный знак, то p3 ≠ p2.

LaTeX

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

Lean4

/-- If the sign of the angle between three points is positive, the last two points are not
equal. -/
theorem right_ne_of_oangle_sign_eq_one {p₁ p₂ p₃ : P} (h : (∡ p₁ p₂ p₃).sign = 1) : p₃ ≠ p₂ :=
  right_ne_of_oangle_sign_ne_zero (h.symm ▸ by decide : (∡ p₁ p₂ p₃).sign ≠ 0)

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