angle_lt_pi_of_not_collinear — Mathlib

English

If three points are not collinear, then the angle ∠ p1 p2 p3 is less than π.

Русский

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

LaTeX

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

Lean4

/-- If three points are not collinear, the angle between them is less than π. -/
theorem angle_lt_pi_of_not_collinear {p₁ p₂ p₃ : P} (h : ¬Collinear ℝ ({ p₁, p₂, p₃ } : Set P)) : ∠ p₁ p₂ p₃ < π :=
  (angle_le_pi _ _ _).lt_of_ne <| angle_ne_pi_of_not_collinear h

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