angle_eq_abs_oangle_toReal — Mathlib

English

The unoriented angle ∠ p1 p p2 equals the absolute value of the oriented angle ∡ p1 p p2.

Русский

Неориентированный угол ∠ p1 p p2 равен модулю ориентированного угла ∡ p1 p p2.

LaTeX

$$$\angle p_1 p p_2 = \left| (\measuredangle p_1 p p_2).toReal \right|$$$

Lean4

/-- The unoriented angle at `p` between two points not equal to `p` is the absolute value of the
oriented angle. -/
theorem angle_eq_abs_oangle_toReal {p p₁ p₂ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) : ∠ p₁ p p₂ = |(∡ p₁ p p₂).toReal| :=
  o.angle_eq_abs_oangle_toReal (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₂)

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