left_ne_right_of_oangle_eq_pi_div_two

English

If the angle equals π/2, the left point differs from the right point.

Русский

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

LaTeX

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

Lean4

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

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