sin_angle_mul_dist_eq_sin_angle_mul_dist

English

In any triangle, the ratio of a side to the sine of the opposite angle is constant.

Русский

В любом треугольнике отношение стороны к синусу противолежащего угла константно.

LaTeX

$$$\frac{\sin(\angle p_1 p_2 p_3)}{\operatorname{dist}(p_2,p_3)} = \frac{\sin(\angle p_3 p_1 p_2)}{\operatorname{dist}(p_3,p_1)}$$$

Lean4

/-- **Law of sines** (sine rule), angle-at-point form. -/
theorem sin_angle_mul_dist_eq_sin_angle_mul_dist (p₁ p₂ p₃ : P) :
    Real.sin (∠ p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (∠ p₃ p₁ p₂) * dist p₃ p₁ :=
  by
  simp only [dist_comm p₂ p₃, angle]
  rw [dist_eq_norm_vsub V p₃ p₂, dist_eq_norm_vsub V p₃ p₁, InnerProductGeometry.angle_comm,
    sin_angle_mul_norm_eq_sin_angle_mul_norm, vsub_sub_vsub_cancel_right, mul_eq_mul_right_iff]
  left
  rw [InnerProductGeometry.angle_comm, ← neg_vsub_eq_vsub_rev p₁ p₂, angle_neg_right, Real.sin_pi_sub]

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