English
For a triangle, twice the circumradius equals the distance between two vertices divided by the sine of the opposite angle.
Русский
Для треугольника удвоенный радиус описанной окружности равен расстоянию между двумя вершинами, делённому на синус противолежащего угла.
LaTeX
$$dist(p1,p3) / |sin(angle(p1,p2,p3))| = 2 · circumradius$$
Lean4
/-- Twice the circumradius of a triangle may be expressed explicitly as 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_eq_two_mul_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_eq_two_mul_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₂₃)
