oangle_eq_angle_or_eq_neg_angle — Mathlib

English

If the sign of the oriented angle is negative, the oriented angle equals the negation of the unoriented angle: o.oangle x y = - UnorientedAngle(x,y).

Русский

Если знак ориентированного угла отрицательный, угол равен противоположному неориентированному углу: o.oangle x y = - unorientedAngle(x,y).

LaTeX

$$$ (o.oangle x y).sign = -1 \Rightarrow o.oangle x y = - InnerProductGeometry.angle x y $$$

Lean4

/-- The oriented angle between two nonzero vectors is plus or minus the unoriented angle. -/
theorem oangle_eq_angle_or_eq_neg_angle {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    o.oangle x y = InnerProductGeometry.angle x y ∨ o.oangle x y = -InnerProductGeometry.angle x y :=
  Real.Angle.cos_eq_real_cos_iff_eq_or_eq_neg.1 <| o.cos_oangle_eq_cos_angle hx hy

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