English
Replacing the first point by the midpoint on the left or replacing the third point by the midpoint on the right leaves the oriented angle unchanged.
Русский
Замена первой точки на середину слева или третьей на середину справа не меняет ориентированный угол.
LaTeX
$$$\angle(\mathrm{midpoint}(p_1,p_2)) p_2 p_3 = \angle p_1 p_2 p_3$ and $\angle p_1 p_2 (\mathrm{midpoint}(p_3,p_2)) = \angle p_1 p_2 p_3$$$
Lean4
/-- Given three points in strict order on the same line, 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_.Sbtw.oangle_sign_eq_left {p₁ p₂ p₃ : P} (p₄ : P) (h : Sbtw ℝ p₁ p₂ p₃) :
(∡ p₁ p₄ p₂).sign = (∡ p₁ p₄ p₃).sign :=
h.wbtw.oangle_sign_eq_of_ne_left _ h.left_ne
