oangle_rotate_sign — Mathlib

English

Swapping the second and third points negates the sign: -(∡ p1 p2 p3).sign = (∡ p1 p3 p2).sign.

Русский

Поменять местами вторую и третью точки меняет знак: −(∡ p1 p2 p3).sign = (∡ p1 p3 p2).sign.

LaTeX

$$$- (\measuredangle p_1 p_2 p_3).sign = (\measuredangle p_1 p_3 p_2).sign$$$

Lean4

/-- Rotating the points in an oriented angle does not change the sign of that angle. -/
theorem oangle_rotate_sign (p₁ p₂ p₃ : P) : (∡ p₂ p₃ p₁).sign = (∡ p₁ p₂ p₃).sign := by
  rw [← oangle_swap₁₂_sign, oangle_swap₁₃_sign]

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