English
Under norm-equality conditions, 2·oangle(y − x1, z − x1) equals 2·oangle(y − x2, z − x2).
Русский
При равенстве норм, 2·угол(y−x1, z−x1) = 2·угол(y−x2, z−x2).
LaTeX
$$$2\\ \\mathrm{oangle}(y - x_1, z - x_1) = 2\\ \\mathrm{oangle}(y - x_2, z - x_2)$$$
Lean4
/-- Oriented 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_eq {s : Sphere P} {p₁ p₂ p₃ p₄ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₄ : p₄ ∈ s)
(hp₂p₁ : p₂ ≠ p₁) (hp₂p₄ : p₂ ≠ p₄) (hp₃p₁ : p₃ ≠ p₁) (hp₃p₄ : p₃ ≠ p₄) :
(2 : ℤ) • ∡ p₁ p₂ p₄ = (2 : ℤ) • ∡ p₁ p₃ p₄ :=
by
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃ hp₄
rw [oangle, oangle, ← vsub_sub_vsub_cancel_right p₁ p₂ s.center, ← vsub_sub_vsub_cancel_right p₄ p₂ s.center,
«o».two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq _ _ _ _ hp₂ hp₃ hp₁ hp₄] <;>
simp [hp₂p₁, hp₂p₄, hp₃p₁, hp₃p₄]
