English
The circumcenter is expressible as a rotated vector from a base to a midpoint, mirroring the tangent-based center formula.
Русский
Центр описанного круга выражается через вращение вектора и середину; аналогично форме через касательную.
LaTeX
$$circumcenter = (tan(angle/2)^{-1}/2) • rotation_{π/2}(p3 - p1) + midpoint(p1,p3)$$
Lean4
/-- The circumcenter of a triangle may be expressed explicitly as a multiple (by half the inverse
of the tangent of the angle at one of the vertices) of a `π / 2` rotation of the vector between
the other two vertices, plus the midpoint of those vertices. -/
theorem inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3}
(h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) :
((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₃) =
t.circumcenter :=
Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center (t.mem_circumsphere _) (t.mem_circumsphere _)
(t.mem_circumsphere _) (t.independent.injective.ne h₁₂) (t.independent.injective.ne h₁₃)
(t.independent.injective.ne h₂₃)
