collinear_of_sin_eq_zero — Mathlib

English

If sin(∠ p1 p2 p3) = 0, then p1, p2, p3 are collinear.

Русский

Если sin(∠ p1 p2 p3) = 0, то точки p1, p2, p3 коллинеарны.

LaTeX

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

Lean4

/-- If the sine of the angle between three points is 0, they are collinear. -/
theorem collinear_of_sin_eq_zero {p₁ p₂ p₃ : P} (h : Real.sin (∠ p₁ p₂ p₃) = 0) :
    Collinear ℝ ({ p₁, p₂, p₃ } : Set P) := by
  revert h
  contrapose
  exact sin_ne_zero_of_not_collinear

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