two_zsmul_oangle_eq_right — Mathlib

English

Replacing the third point by a collinear third point with opposite ray yields the same twice-angle.

Русский

Замена третьей точки на другую точку на той же прямой с противоположного ray сохраняет удвоенный угол.

LaTeX

$$$Collinear_\mathbb{R}({p_3,p_2,p_3'}) \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 third point by one on the same line does not change twice the oriented angle. -/
theorem _root_.Collinear.two_zsmul_oangle_eq_right {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
  rw [oangle_rev, smul_neg, h.two_zsmul_oangle_eq_left hp₃p₂ hp₃'p₂, ← smul_neg, ← oangle_rev]

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