oangle_eq_angle_or_eq_neg_angle — Mathlib

English

For three points p1, p, p2 with p1 ≠ p and p2 ≠ p, the oriented angle ∡ p1 p p2 is either equal to the unoriented angle ∠ p1 p p2 or equal to its negation.

Русский

Пусть p1, p, p2 — точки, и p1 ≠ p, p2 ≠ p. Тогда ореинтированный угол ∡ p1 p p2 равен либо неориентированному углу ∠ p1 p p2, либо противоположному ему.

LaTeX

$$$\measuredangle p_1 p p_2 = \angle p_1 p p_2 \quad\lor\quad \measuredangle p_1 p p_2 = -\angle p_1 p p_2$$$

Lean4

/-- The oriented angle at `p` between two points not equal to `p` is plus or minus the unoriented
angle. -/
theorem oangle_eq_angle_or_eq_neg_angle {p p₁ p₂ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) :
    ∡ p₁ p p₂ = ∠ p₁ p p₂ ∨ ∡ p₁ p p₂ = -∠ p₁ p p₂ :=
  o.oangle_eq_angle_or_eq_neg_angle (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₂)

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