sin_angle_div_norm_eq_sin_angle_div_norm

English

A variant of the sine rule with division by norms: sin(angle x,y)/‖x−y‖ = sin(angle y,(x−y))/‖x‖, under nondegeneracy conditions.

Русский

Вариант закона синусов с делением на нормы: sin(angle x,y)/‖x−y‖ = sin(angle y,(x−y))/‖x‖ при невыраженных случаев.

LaTeX

$$$\dfrac{\sin(\angle x,y)}{\|x-y\|} = \dfrac{\sin(\angle y,(x-y))}{\|x\|}$$$

Lean4

/-- A variant of the law of sines, (two given sides are nonzero), vector angle form. -/
theorem sin_angle_div_norm_eq_sin_angle_div_norm (x y : V) (hx : x ≠ 0) (hxy : x - y ≠ 0) :
    Real.sin (angle x y) / ‖x - y‖ = Real.sin (angle y (x - y)) / ‖x‖ := by
  simp [field, sin_angle_mul_norm_eq_sin_angle_mul_norm x y]

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