oangle_eq_angle_of_sign_eq_one — Mathlib

English

If two unoriented angles are equal and the signs of the corresponding oriented angles are equal, then the oriented angles are equal (and conversely).

Русский

Если неориентированные углы равны и знаки соответствующих ориентированных углов равны, то ориентированные углы равны, и наоборот.

LaTeX

$$$\angle p_1 p_2 p_3 = \angle p_4 p_5 p_6 \iff (\measuredangle p_1 p_2 p_3).sign = (\measuredangle p_4 p_5 p_6).sign \Rightarrow \measuredangle p_1 p_2 p_3 = \measuredangle p_4 p_5 p_6$$$

Lean4

/-- The oriented angle between three points equals the unoriented angle if the sign is
positive. -/
theorem oangle_eq_angle_of_sign_eq_one {p₁ p₂ p₃ : P} (h : (∡ p₁ p₂ p₃).sign = 1) : ∡ p₁ p₂ p₃ = ∠ p₁ p₂ p₃ :=
  o.oangle_eq_angle_of_sign_eq_one h

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