oangle — Mathlib

English

The oriented angle ∡A B C is defined as the oriented angle between the translated vectors AB and CB at B, using the fixed orientation.

Русский

Ориентированный угол ∡A B C определяется как угол между векторами AB и CB, полученными переносом в точку B с учётом фиксированной ориентации.

LaTeX

$$$\\angle p_1 p_2 p_3 = o.oangle(p_1 - p_2, p_3 - p_2)$$$

Lean4

/-- The oriented angle at `p₂` between the line segments to `p₁` and `p₃`, modulo `2 * π`. If
either of those points equals `p₂`, this is 0. See `EuclideanGeometry.angle` for the
corresponding unoriented angle definition. -/
def oangle (p₁ p₂ p₃ : P) : Real.Angle :=
  o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

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