angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two

English

If the oriented angle equals π/2, then the reversed orientation has the unoriented angle equal to π/2.

Русский

Если ориентированный угол равен π/2, то развёрнутая ориентация тоже даёт неориентированный π/2.

LaTeX

$$$\angle p_3 p_2 p_1 = \dfrac{\pi}{2} \;\text{if}\; \measuredangle p_1 p_2 p_3 = \dfrac{\pi}{2}$$$

Lean4

/-- If the oriented angle between three points is `π / 2`, so is the unoriented angle
(reversed). -/
theorem angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    ∠ p₃ p₂ p₁ = π / 2 := by
  rw [angle_comm]
  exact angle_eq_pi_div_two_of_oangle_eq_pi_div_two h

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