oangle_swap₁₃_sign — Mathlib

English

As above: swapping the first two points flips the sign.

Русский

Как и выше: перестановка первых двух точек меняет знак.

LaTeX

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

Lean4

/-- Swapping the first 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_rev, Real.Angle.sign_neg, neg_neg]

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