sin_ne_zero_of_not_collinear — Mathlib

English

If three points are not collinear, the sine of the angle between them is nonzero.

Русский

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

LaTeX

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

Lean4

/-- If three points are not collinear, the sine of the angle between them is nonzero. -/
theorem sin_ne_zero_of_not_collinear {p₁ p₂ p₃ : P} (h : ¬Collinear ℝ ({ p₁, p₂, p₃ } : Set P)) :
    Real.sin (∠ p₁ p₂ p₃) ≠ 0 :=
  ne_of_gt (sin_pos_of_not_collinear h)

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