English
The center of the circle through p1 and p2 can be expressed as a combination of a π/2 rotation of p2−p1 scaled by tan(∡ p2 p1 s.center)/2 plus the midpoint of p1 and p2.
Русский
Центр окружности через p1 и p2 выражается как линейная комбинация: половинное тангенс угла умноженное на вращение π/2 применённое к вектору p2−p1 плюс середина p1 и p2.
LaTeX
$$$(\\tan(\\angle p_2 p_1 s.center)/2) \\cdot \\, o.rotation_{\\pi/2}(p_2 - p_1) + \\text{midpoint}(p_1,p_2) = s.center$$$
Lean4
/-- Twice a base angle of an isosceles triangle with apex at the center of a circle, plus twice
the angle at the apex of a triangle with the same base but apex on the circle, equals `π`. -/
theorem two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi {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₃) :
(2 : ℤ) • ∡ p₃ p₁ s.center + (2 : ℤ) • ∡ p₁ p₂ p₃ = π := by
rw [← oangle_center_eq_two_zsmul_oangle hp₁ hp₂ hp₃ hp₂p₁ hp₂p₃,
oangle_eq_pi_sub_two_zsmul_oangle_center_right hp₁ hp₃ hp₁p₃, add_sub_cancel]
