left_ne_right_of_oangle_eq_pi — Mathlib

English

If the angle equals π, then the left and right points cannot be equal.

Русский

Если угол равен π, левая и правая точки не могут совпадать.

LaTeX

$$$\\angle p_1 p_2 p_3 = \\pi \\Rightarrow p_1 \\neq p_3$$$

Lean4

/-- If the angle between three points is `π`, the first and third points are not equal. -/
theorem left_ne_right_of_oangle_eq_pi {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = π) : p₁ ≠ p₃ :=
  left_ne_right_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_ne_zero : ∡ p₁ p₂ p₃ ≠ 0)

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