sin_angle_add — Mathlib

English

The sine of the angle between x and x+y equals the corresponding Gram determinant expression divided by the product of norms of x and x+y.

Русский

Синус угла между x и x+y равен соответствующему выражению детерминанта Грамма, деленному на произведение норм x и (x+y).

LaTeX

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

Lean4

/-- The sine of the angle between `x` and `x + y`. -/
theorem sin_angle_add {x y : V} (hx : x ≠ 0) (hy : x + y ≠ 0) :
    Real.sin (angle x (x + y)) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖) :=
  by
  rw [sin_angle hx hy]
  field_simp
  simp only [inner_add_left, inner_add_right, real_inner_comm]
  ring_nf

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