sin_angle — Mathlib

English

The sine of the angle between x and y equals the square root expression divided by the product of their norms, provided x,y ≠ 0.

Русский

Синус угла между x и y равен корню из выражения, деленному на произведение норм x и y, при условии x ≠ 0, y ≠ 0.

LaTeX

$$$\\\\sin(\\\\angle x y) = \\\\sqrt{\\\\⟪x, x\\\\⟫ \\\\cdot \\\\⟪y, y\\\\⟫ - \\\\⟪x, y\\\\⟫^2} / ( \\\\|x\\\\| \\\\cdot \\\\|y\\\\| )$$$

Lean4

/-- The sine of the angle between two vectors. -/
theorem sin_angle {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) :=
  by
  rw [← sin_angle_mul_norm_mul_norm]
  field_simp

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