English
If the lines determined by p1 p2 and p4 p5 are parallel and the lines determined by p3 p2 and p6 p5 are parallel, then twice the oangle p1 p2 p3 equals twice the oangle p4 p5 p6.
Русский
Если прямые, проходящие через p1,p2 и через p4,p5, параллельны, а прямые через p3,p2 и через p6,p5 — тоже параллельны, то 2·∡ p1 p2 p3 = 2·∡ p4 p5 p6.
LaTeX
$$$ (AffineSubspace\!\{p_1,p_2\} \parallel AffineSubspace\!\{p_4,p_5\}) \land (AffineSubspace\!\{p_3,p_2\} \parallel AffineSubspace\!\{p_6,p_5\}) \Rightarrow (2 : \mathbb{Z}) \!\cdot \angle p_1 p_2 p_3 = (2 : \mathbb{Z}) \!\cdot \angle p_4 p_5 p_6 $$$
Lean4
/-- If twice the oriented angles between two triples of points are equal, one triple is collinear
if and only if the other is. -/
theorem collinear_iff_of_two_zsmul_oangle_eq {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h : (2 : ℤ) • ∡ p₁ p₂ p₃ = (2 : ℤ) • ∡ p₄ p₅ p₆) :
Collinear ℝ ({ p₁, p₂, p₃ } : Set P) ↔ Collinear ℝ ({ p₄, p₅, p₆ } : Set P) := by
simp_rw [← oangle_eq_zero_or_eq_pi_iff_collinear, ← Real.Angle.two_zsmul_eq_zero_iff, h]
