angle_eq_pi_div_two_of_oangle_eq_pi_div_two

English

If the oriented angle equals π/2, then the unoriented angle equals π/2.

Русский

Если ориентированный угол равен π/2, то неориентированный угол равен π/2.

LaTeX

$$$\measuredangle p_1 p_2 p_3 = \dfrac{\pi}{2} \Rightarrow \angle p_1 p_2 p_3 = \dfrac{\pi}{2}$$$

Lean4

/-- If the oriented angle between three points is `π / 2`, so is the unoriented angle. -/
theorem angle_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, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
  exact o.inner_eq_zero_of_oangle_eq_pi_div_two h

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