oangle_swap₂₃_sign — Mathlib

English

Rotating the points in an oriented angle does not change the sign: (∡ p2 p3 p1).sign = (∡ p1 p2 p3).sign.

Русский

Поворот трёх точек в ориентированном угле не меняет знак: (∡ p2 p3 p1).sign = (∡ p1 p2 p3).sign.

LaTeX

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

Lean4

/-- Swapping the second and third points in an oriented angle negates the sign of that angle. -/
theorem oangle_swap₂₃_sign (p₁ p₂ p₃ : P) : -(∡ p₁ p₂ p₃).sign = (∡ p₁ p₃ p₂).sign := by
  rw [oangle_swap₁₃_sign, ← oangle_swap₁₂_sign, oangle_swap₁₃_sign]

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