oangle_rev — Mathlib

English

The oriented angle reverses sign when the order of the three points is reversed: ∡ p3 p2 p1 = - ∡ p1 p2 p3.

Русский

Оріентированный угол меняет знак при обратном порядке трёх точек: ∡ p3 p2 p1 = − ∡ p1 p2 p3.

LaTeX

$$$ ∡ p_3 p_2 p_1 = -\ ∡ p_1 p_2 p_3 $$$

Lean4

/-- Reversing the order of the points passed to `oangle` negates the angle. -/
theorem oangle_rev (p₁ p₂ p₃ : P) : ∡ p₃ p₂ p₁ = -∡ p₁ p₂ p₃ :=
  o.oangle_rev _ _

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