oangle_eq_zero_or_eq_pi_iff_collinear

English

If twice the oriented angles of two triples are equal, the first triple is affinely independent if and only if the second triple is.

Русский

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

LaTeX

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

Lean4

/-- An oriented angle is zero or `π` if and only if the three points are collinear. -/
theorem oangle_eq_zero_or_eq_pi_iff_collinear {p₁ p₂ p₃ : P} :
    ∡ p₁ p₂ p₃ = 0 ∨ ∡ p₁ p₂ p₃ = π ↔ Collinear ℝ ({ p₁, p₂, p₃ } : Set P) := by
  rw [← not_iff_not, not_or, oangle_ne_zero_and_ne_pi_iff_affineIndependent, affineIndependent_iff_not_collinear_set]

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