left_ne_right_of_oangle_ne_zero — Mathlib

English

If the angle is π/2, the first two points are not equal.

Русский

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

LaTeX

$$$\\angle p_1 p_2 p_3 = \\frac{\\pi}{2} \\Rightarrow p_1 \\neq p_2$$$

Lean4

/-- If the angle between three points is nonzero, the first and third points are not equal. -/
theorem left_ne_right_of_oangle_ne_zero {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ ≠ 0) : p₁ ≠ p₃ := by
  rw [← (vsub_left_injective p₂).ne_iff]; exact o.ne_of_oangle_ne_zero h

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