right_ne_of_oangle_ne_zero — Mathlib

English

If the angle is exactly π, the first two points are distinct.

Русский

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

LaTeX

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

Lean4

/-- If the angle between three points is nonzero, the last two points are not equal. -/
theorem right_ne_of_oangle_ne_zero {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ ≠ 0) : p₃ ≠ p₂ := by rw [← @vsub_ne_zero V];
  exact o.right_ne_zero_of_oangle_ne_zero h

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