collinear_of_angle_eq_pi — Mathlib

English

If the angle ∠ p1 p2 p3 = π, then p1, p2, p3 are collinear.

Русский

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

LaTeX

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

Lean4

/-- If the angle between three points is π, they are collinear. -/
theorem collinear_of_angle_eq_pi {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π) : Collinear ℝ ({ p₁, p₂, p₃ } : Set P) :=
  collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi.2 <| Or.inr <| Or.inr <| Or.inr h

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