English
For any x,y in a 2D oriented space, the sign of o.oangle((−x) + y, y) equals the sign of o.oangle(x,y).
Русский
Для любых x,y знак o.oangle((−x) + y, y) равен знаку o.oangle(x,y).
LaTeX
$$$\\forall x,y\\in V,\\ o.oangle(-x + y, y).sign = o.oangle(x,y).sign$$$
Lean4
/-- A base angle of an isosceles triangle is acute, oriented vector angle form. -/
theorem abs_oangle_sub_left_toReal_lt_pi_div_two {x y : V} (h : ‖x‖ = ‖y‖) : |(o.oangle (y - x) y).toReal| < π / 2 :=
by
by_cases hn : x = y; · simp [hn, Real.pi_pos]
have hs : ((2 : ℤ) • o.oangle (y - x) y).sign = (o.oangle (y - x) y).sign :=
by
conv_rhs => rw [oangle_sign_sub_left_swap]
rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hn h, Real.Angle.sign_pi_sub]
rw [Real.Angle.sign_two_zsmul_eq_sign_iff] at hs
rcases hs with (hs | hs)
· rw [oangle_eq_pi_iff_oangle_rev_eq_pi, oangle_eq_pi_iff_sameRay_neg, neg_sub] at hs
rcases hs with ⟨hy, -, hr⟩
rw [← exists_nonneg_left_iff_sameRay hy] at hr
rcases hr with ⟨r, hr0, hr⟩
rw [eq_sub_iff_add_eq] at hr
nth_rw 2 [← one_smul ℝ y] at hr
rw [← add_smul] at hr
rw [← hr, norm_smul, Real.norm_eq_abs, abs_of_pos (Left.add_pos_of_nonneg_of_pos hr0 one_pos), mul_left_eq_self₀,
or_iff_left (norm_ne_zero_iff.2 hy), add_eq_right] at h
rw [h, zero_add, one_smul] at hr
exact False.elim (hn hr.symm)
· exact hs
