sin_angle_div_dist_eq_sin_angle_div_dist

English

If three points are non-collinear, then sin(angle at p1p2p3) scaled by distance equals sin of another angle times the opposite distance.

Русский

Если три точки не лежат на одной прямой, то синус угла, умноженный на расстояние, равен синусу другого угла, умноженному на противоположное расстояние.

LaTeX

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

Lean4

/-- A variant of the law of sines, angle-at-point form. -/
theorem sin_angle_div_dist_eq_sin_angle_div_dist {p₁ p₂ p₃ : P} (h23 : p₂ ≠ p₃) (h31 : p₃ ≠ p₁) :
    Real.sin (∠ p₁ p₂ p₃) / dist p₃ p₁ = Real.sin (∠ p₃ p₁ p₂) / dist p₂ p₃ :=
  by
  simp [field, dist_ne_zero.mpr h23, dist_ne_zero.mpr h31, mul_comm (dist ..)]
  exact law_sin _ _ _

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