English
The circumradius of a triangle can be expressed as half a side length divided by the sine of the opposite angle.
Русский
Описанная окружность треугольника выражается через половину стороны и синус противолежащего угла.
LaTeX
$$dist(p1,p3) / |sin(angle(p1,p2,p3))| = 2 · circumradius$$
Lean4
/-- The circumradius of a triangle may be expressed explicitly as half the length of a side
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_circumradius (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂)
(h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) :
dist (t.points i₁) (t.points i₃) / |Real.Angle.sin (∡ (t.points i₁) (t.points i₂) (t.points i₃))| / 2 =
t.circumradius :=
Sphere.dist_div_sin_oangle_div_two_eq_radius (t.mem_circumsphere _) (t.mem_circumsphere _) (t.mem_circumsphere _)
(t.independent.injective.ne h₁₂) (t.independent.injective.ne h₁₃) (t.independent.injective.ne h₂₃)
