English
Replacing the first point by the midpoint of the segment to the second point leaves the oriented angle unchanged: ∡(midpoint p1 p2) p2 p3 = ∡ p1 p2 p3.
Русский
Замещая первую точку серединой отрезка к второй точке, ориентированный угол не меняется: ∡(midpoint p1 p2) p2 p3 = ∡ p1 p2 p3.
LaTeX
$$$\angle(\mathrm{midpoint}(p_1,p_2))\; p_2\; p_3 = \angle p_1\; p_2\; p_3$$$
Lean4
/-- An oriented angle is unchanged by replacing the first point by one weakly further away on the
same ray. -/
theorem _root_.Wbtw.oangle_eq_left {p₁ p₁' p₂ p₃ : P} (h : Wbtw ℝ p₂ p₁ p₁') (hp₁p₂ : p₁ ≠ p₂) :
∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃ := by
by_cases hp₃p₂ : p₃ = p₂; · simp [hp₃p₂]
by_cases hp₁'p₂ : p₁' = p₂; · rw [hp₁'p₂, wbtw_self_iff] at h; exact False.elim (hp₁p₂ h)
rw [← oangle_add hp₁'p₂ hp₁p₂ hp₃p₂, h.oangle₃₁₂_eq_zero, zero_add]
