oangle_sign_eq_zero_iff_collinear

English

If twice the oriented angles p1 p2 p3 and p4 p5 p6 are equal, then the triples are collinear in the same sense.

Русский

Если дважды равны ориентированные углы двух троек, то тройки точек коллинеарны взаимно согласованно.

LaTeX

$$$ (2 : \mathbb{Z}) \!\cdot \angle p_1 p_2 p_3 = (2 : \mathbb{Z}) \!\cdot \angle p_4 p_5 p_6 \Rightarrow (Collinear \mathbb{R} \{p_1,p_2,p_3\}) \iff (Collinear \mathbb{R} \{p_4,p_5,p_6\})$$$

Lean4

/-- An oriented angle has a sign zero if and only if the three points are collinear. -/
theorem oangle_sign_eq_zero_iff_collinear {p₁ p₂ p₃ : P} :
    (∡ p₁ p₂ p₃).sign = 0 ↔ Collinear ℝ ({ p₁, p₂, p₃ } : Set P) := by
  rw [Real.Angle.sign_eq_zero_iff, oangle_eq_zero_or_eq_pi_iff_collinear]

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