angle_ne_zero_of_not_collinear — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If three points are not collinear, the angle between them is nonzero. -/
theorem angle_ne_zero_of_not_collinear {p₁ p₂ p₃ : P} (h : ¬Collinear ℝ ({ p₁, p₂, p₃ } : Set P)) : ∠ p₁ p₂ p₃ ≠ 0 :=
  mt collinear_of_angle_eq_zero h

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