English
For four points x1, x2, y, z on a circle lying on the same circle, with all four on the circle and certain non-degeneracy conditions, 2·oangle(y−x1, z−x1) = 2·oangle(y−x2, z−x2).
Русский
Для четырёх точек x1, x2, y, z на окружности, при некоторых непустых условиях, выполняется равенство двухкратных ориентированных углов.
LaTeX
$$$2\\ \\mathrm{oangle}(y - x_1, z - x_1) = 2\\ \\mathrm{oangle}(y - x_2, z - x_2)$ при равенстве норм и непустых условиях между точками.$$
Lean4
/-- Oriented vector angle version of "angles in same segment are equal" and "opposite angles of
a cyclic quadrilateral add to π", for oriented angles mod π (for which those are the same
result), represented here as equality of twice the angles. -/
theorem two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq {x₁ x₂ y z : V} (hx₁yne : x₁ ≠ y) (hx₁zne : x₁ ≠ z)
(hx₂yne : x₂ ≠ y) (hx₂zne : x₂ ≠ z) {r : ℝ} (hx₁ : ‖x₁‖ = r) (hx₂ : ‖x₂‖ = r) (hy : ‖y‖ = r) (hz : ‖z‖ = r) :
(2 : ℤ) • o.oangle (y - x₁) (z - x₁) = (2 : ℤ) • o.oangle (y - x₂) (z - x₂) :=
o.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real hx₁yne hx₁zne hx₁ hy hz ▸
o.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real hx₂yne hx₂zne hx₂ hy hz
