English
Let t be a triangle in a two-dimensional Euclidean setting. The circumsphere of t can be written explicitly using two vertices and the angle at the third vertex. In particular, its center is a combination of a 90-degree rotation of the vector between the two chosen vertices and their midpoint, scaled by the reciprocal of the tangent of the angle at the third vertex, and its radius depends on the distance between the two chosen vertices and the sine of that angle.
Русский
Пусть t — треугольник в евклидовом пространстве размерности 2. Описанная сфера треугольника может быть выражена явно через две вершины и угол при третьей вершине. В частности, центр сферы задаётся комбинацией вращения на 90 градусов вектора между двумя выбранными вершинами и их середины, масштабированной обратной величиной тангенса угла при третьей вершине, а радиус определяется расстоянием между этими двумя вершинами и синусом этого угла.
LaTeX
$$$\text{Circumsphere}(t) = \langle c, R \rangle$, где
\(\theta = ∡(t.points i_1)(t.points i_2)(t.points i_3)\),
c = ((\tan θ)^{-1} / 2) · R_{π/2}(t.points i_3 - t.points i_1) + midpoint ℝ (t.points i_1) (t.points i_3),
R = d(t.points i_1, t.points i_3) / (2|\sin θ|).$$
Lean4
/-- The circumsphere of a triangle may be expressed explicitly in terms of two points and the
angle at the third point. -/
theorem circumsphere_eq_of_dist_of_oangle (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃)
(h₂₃ : i₂ ≠ i₃) :
t.circumsphere =
⟨((Real.Angle.tan (∡ (t.points i₁) (t.points i₂) (t.points i₃)))⁻¹ / 2) •
«o».rotation (π / 2 : ℝ) (t.points i₃ -ᵥ t.points i₁) +ᵥ
midpoint ℝ (t.points i₁) (t.points i₃),
dist (t.points i₁) (t.points i₃) / |Real.Angle.sin (∡ (t.points i₁) (t.points i₂) (t.points i₃))| / 2⟩ :=
t.circumsphere.ext (t.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter h₁₂ h₁₃ h₂₃).symm
(t.dist_div_sin_oangle_div_two_eq_circumradius h₁₂ h₁₃ h₂₃).symm
