collinear_iff_eq_or_eq_or_sin_eq_zero

English

Three points are collinear iff either p1 = p2, or p3 = p2, or sin(∠ p1 p2 p3) = 0.

Русский

Три точки коллинеарны тогда и только тогда, когда либо p1=p2, либо p3=p2, либо sin(∠ p1 p2 p3) = 0.

LaTeX

$$$$ \operatorname{Collinear}_{\mathbb{R}}(\{p_1,p_2,p_3\}) \iff p_1=p_2 \lor p_3=p_2 \lor \sin(\angle p_1 p_2 p_3)=0. $$$$

Lean4

/-- Three points are collinear if and only if the first or third point equals the second or
the sine of the angle between three points is zero. -/
theorem collinear_iff_eq_or_eq_or_sin_eq_zero {p₁ p₂ p₃ : P} :
    Collinear ℝ ({ p₁, p₂, p₃ } : Set P) ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ Real.sin (∠ p₁ p₂ p₃) = 0 := by
  rw [sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi, collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi]

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