English
For three points on a circle, the chord length relates to the radius by the sine of the opposite angle.
Русский
Для трёх точек на окружности сторона соотв. углу связана с радиусом через синус противоположного угла.
LaTeX
$$$\\frac{\\text{dist}(p_1,p_3)}{|\\sin(\\angle p_1 p_2 p_3)|} = 2 \\cdot \\text{radius}$$$
Lean4
/-- Given three points on a circle, the radius of that circle may be expressed explicitly as half
the distance between two of those points divided by the absolute value of the sine of the angle
at the third point (a version of the law of sines or sine rule). -/
theorem dist_div_sin_oangle_div_two_eq_radius {s : Sphere P} {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s)
(hp₁p₂ : p₁ ≠ p₂) (hp₁p₃ : p₁ ≠ p₃) (hp₂p₃ : p₂ ≠ p₃) : dist p₁ p₃ / |Real.Angle.sin (∡ p₁ p₂ p₃)| / 2 = s.radius :=
by
convert dist_div_cos_oangle_center_div_two_eq_radius hp₁ hp₃ hp₁p₃
rw [←
Real.Angle.abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi
(two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi hp₁ hp₂ hp₃ hp₁p₂.symm hp₂p₃ hp₁p₃),
abs_of_nonneg (Real.Angle.cos_nonneg_iff_abs_toReal_le_pi_div_two.2 _)]
exact (abs_oangle_center_right_toReal_lt_pi_div_two hp₁ hp₃).le
