English
Let V be a 2-dimensional normed vector space with an orientation. If x, y, z ∈ V are pairwise distinct and have the same norm, then the oriented angle at y and z equals twice the oriented angle at (y − x) and (z − x).
Русский
Пусть V — двумерное нормированное векторное пространство с ориентировкой. Пусть x, y, z ∈ V попарно различны и имеют одинаковую норму. Тогда ориентированный угол y-z равен двум ориентированным углу (y−x)−(z−x).
LaTeX
$$$\\mathrm{oangle}(y,z) = 2\\ \\mathrm{oangle}(y - x, z - x)$, при условиях $x \\neq y$, $x \\neq z$, и $\\|x\\| = \\|y\\| = \\|z\\|$.$$
Lean4
/-- Angle at center of a circle equals twice angle at circumference, oriented vector angle
form. -/
theorem oangle_eq_two_zsmul_oangle_sub_of_norm_eq {x y z : V} (hxyne : x ≠ y) (hxzne : x ≠ z) (hxy : ‖x‖ = ‖y‖)
(hxz : ‖x‖ = ‖z‖) : o.oangle y z = (2 : ℤ) • o.oangle (y - x) (z - x) :=
by
have hy : y ≠ 0 := by
rintro rfl
rw [norm_zero, norm_eq_zero] at hxy
exact hxyne hxy
have hx : x ≠ 0 := norm_ne_zero_iff.1 (hxy.symm ▸ norm_ne_zero_iff.2 hy)
have hz : z ≠ 0 := norm_ne_zero_iff.1 (hxz ▸ norm_ne_zero_iff.2 hx)
calc
o.oangle y z = o.oangle x z - o.oangle x y := (o.oangle_sub_left hx hy hz).symm
_ = π - (2 : ℤ) • o.oangle (x - z) x - (π - (2 : ℤ) • o.oangle (x - y) x) := by
rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxzne.symm hxz.symm,
o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hxyne.symm hxy.symm]
_ = (2 : ℤ) • (o.oangle (x - y) x - o.oangle (x - z) x) := by abel
_ = (2 : ℤ) • o.oangle (x - y) (x - z) := by
rw [o.oangle_sub_right (sub_ne_zero_of_ne hxyne) (sub_ne_zero_of_ne hxzne) hx]
_ = (2 : ℤ) • o.oangle (y - x) (z - x) := by rw [← oangle_neg_neg, neg_sub, neg_sub]
