angle_pos_of_not_collinear — Mathlib

English

If three points are not collinear, then the angle ∠ p1 p2 p3 is strictly greater than 0.

Русский

Если три точки не лежат на одной прямой, угол ∠ p1 p2 p3 положителен.

LaTeX

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

Lean4

/-- If three points are not collinear, the angle between them is positive. -/
theorem angle_pos_of_not_collinear {p₁ p₂ p₃ : P} (h : ¬Collinear ℝ ({ p₁, p₂, p₃ } : Set P)) : 0 < ∠ p₁ p₂ p₃ :=
  (angle_nonneg _ _ _).lt_of_ne (angle_ne_zero_of_not_collinear h).symm

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