oangle_eq_of_angle_eq_of_sign_eq — Mathlib

English

If two unoriented angles are equal and the signs of the corresponding oriented angles are equal, then the oriented angles themselves are equal.

Русский

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

LaTeX

$$$\angle p_1 p_2 p_3 = \angle p_4 p_5 p_6 \land (\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

/-- If two unoriented angles are equal, and the signs of the corresponding oriented angles are
equal, then the oriented angles are equal (even in degenerate cases). -/
theorem oangle_eq_of_angle_eq_of_sign_eq {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆)
    (hs : (∡ p₁ p₂ p₃).sign = (∡ p₄ p₅ p₆).sign) : ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ :=
  o.oangle_eq_of_angle_eq_of_sign_eq h hs

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