angle — Mathlib

English

The cosine of the angle between two vectors x and y is equal to ⟪x,y⟫ divided by (||x|| · ||y||).

Русский

Косинус угла между двумя векторами x и y равен ⟪x,y⟫ делить на (||x|| · ||y||).

LaTeX

$$$$ \cos(\angle x,y) = \frac{\langle x,y\rangle}{\|x\| \cdot \|y\|}. $$$$

Lean4

/-- The undirected angle between two vectors. If either vector is 0,
this is π/2. See `Orientation.oangle` for the corresponding oriented angle
definition. -/
def angle (x y : V) : ℝ :=
  Real.arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))

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