oangle_eq_neg_angle_of_sign_eq_neg_one

English

If the sign of the oriented angle ∡ p1 p2 p3 is -1, then ∡ p1 p2 p3 = - ∠ p1 p2 p3.

Русский

Если знак ориентированного угла ∡ p1 p2 p3 равен -1, то ∡ p1 p2 p3 = - ∠ p1 p2 p3.

LaTeX

$$$(\measuredangle p_1 p_2 p_3).\text{sign} = -1 \Rightarrow \measuredangle p_1 p_2 p_3 = -\angle p_1 p_2 p_3$$$

Lean4

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

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