sin_pos_of_not_collinear — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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