English
Let o be an orientation of a 2-dimensional real vector space V, and let x,y ∈ V be nonzero with x ≠ y and with ‖x‖ = ‖y‖. Then the apex angle relation holds: the oriented angle from y to x equals π minus twice the oriented base angle, i.e. o.oangle y x = π − 2 o.oangle (y − x) y.
Русский
Пусть o — ориентирование двумерного вещественного вектора V, возьмем x,y ∈ V такие, что x ≠ y и ‖x‖ = ‖y‖. Тогда угол вершины равен π минус вдвое большему ориентированному углу между y−x и y: o.oangle y x = π − 2 o.oangle (y − x) y.
LaTeX
$$$ x \neq y \land \|x\| = \|y\| \Rightarrow o.oangle y x = \pi - 2\, o.oangle (y - x) y $$$
Lean4
/-- The angle at the apex of an isosceles triangle is `π` minus twice a base angle, oriented
vector angle form. -/
theorem oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq {x y : V} (hn : x ≠ y) (h : ‖x‖ = ‖y‖) :
o.oangle y x = π - (2 : ℤ) • o.oangle (y - x) y :=
by
rw [two_zsmul]
nth_rw 1 [← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]
rw [eq_sub_iff_add_eq, ← oangle_neg_neg, ← add_assoc]
have hy : y ≠ 0 := by
rintro rfl
rw [norm_zero, norm_eq_zero] at h
exact hn h
have hx : x ≠ 0 := norm_ne_zero_iff.1 (h.symm ▸ norm_ne_zero_iff.2 hy)
convert o.oangle_add_cyc3_neg_right (neg_ne_zero.2 hy) hx (sub_ne_zero_of_ne hn.symm) using 1
simp
