English
If x1, x2, y, z lie at the same distance r from the origin and x1, x2, y, z are all distinct, then 2·angle(y − x1, z − x1) equals 2·angle(y − x2, z − x2).
Русский
Если точки x1, x2, y, z лежат на окружности радиуса r и попарно различны, то дважды угол между y − x1 и z − x1 равен дважды углу между y − x2 и z − x2.
LaTeX
$$$2\\ \\mathrm{oangle}(y - x_1, z - x_1) = 2\\ \\mathrm{oangle}(y - x_2, z - x_2)$, при предположениях $\\|x_1\\| = \\|x_2\\| = r$ и $\\|y\\| = \\|z\\| = r$, $x_1 \\neq y$, $x_1 \\neq z$, $x_2 \\neq y$, $x_2 \\neq z$.$$
Lean4
/-- Angle at center of a circle equals twice angle at circumference, oriented vector angle
form with radius specified. -/
theorem oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real {x y z : V} (hxyne : x ≠ y) (hxzne : x ≠ z) {r : ℝ}
(hx : ‖x‖ = r) (hy : ‖y‖ = r) (hz : ‖z‖ = r) : o.oangle y z = (2 : ℤ) • o.oangle (y - x) (z - x) :=
o.oangle_eq_two_zsmul_oangle_sub_of_norm_eq hxyne hxzne (hy.symm ▸ hx) (hz.symm ▸ hx)
