English
If p1, p2, p1' are collinear and p1' ≠ p2, then (2)•oangle(p1,p2,p3) = (2)•oangle(p1',p2,p3).
Русский
Если p1, p2, p1' коллинеарны и p1' ≠ p2, то дважды угол не меняется: 2·∡ p1 p2 p3 = 2·∡ p1' p2 p3.
LaTeX
$$$Collinear_\mathbb{R}({p_1,p_2,p_1'}) \Rightarrow (2:\mathbb{Z})\cdot \angle p_1 p_2 p_3 = (2:\mathbb{Z})\cdot \angle p_1' p_2 p_3$$$
Lean4
/-- Replacing the first point by one on the same line does not change twice the oriented angle. -/
theorem _root_.Collinear.two_zsmul_oangle_eq_left {p₁ p₁' p₂ p₃ : P} (h : Collinear ℝ ({ p₁, p₂, p₁' } : Set P))
(hp₁p₂ : p₁ ≠ p₂) (hp₁'p₂ : p₁' ≠ p₂) : (2 : ℤ) • ∡ p₁ p₂ p₃ = (2 : ℤ) • ∡ p₁' p₂ p₃ :=
by
by_cases hp₃p₂ : p₃ = p₂; · simp [hp₃p₂]
rcases h.wbtw_or_wbtw_or_wbtw with (hw | hw | hw)
· have hw' : Sbtw ℝ p₁ p₂ p₁' := ⟨hw, hp₁p₂.symm, hp₁'p₂.symm⟩
rw [hw'.oangle_eq_add_pi_left hp₃p₂, smul_add, Real.Angle.two_zsmul_coe_pi, add_zero]
· rw [hw.oangle_eq_left hp₁'p₂]
· rw [hw.symm.oangle_eq_left hp₁p₂]
