English
The circumcenter of a triangle lies at a point expressible via a rotation and a midpoint combination, analogous to the tangent-based center formula.
Русский
Центр окружности треугольника задаётся через вращение и середину, аналогично формуле через касательную.
LaTeX
$$центр = tan-based-rotation-комбинация(точки) + середина$$
Lean4
/-- Given three points on a circle, the center of that circle may be expressed explicitly as a
multiple (by half the inverse of the tangent of the angle at one of those points) of a `π / 2`
rotation of the vector between the other two points, plus the midpoint of those points. -/
theorem inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center {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₃) :
((Real.Angle.tan (∡ p₁ p₂ p₃))⁻¹ / 2) • «o».rotation (π / 2 : ℝ) (p₃ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₃ = s.center :=
by
convert tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center hp₁ hp₃ hp₁p₃
convert (Real.Angle.tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi _).symm
rw [add_comm, two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi hp₁ hp₂ hp₃ hp₁p₂.symm hp₂p₃ hp₁p₃]
