English
Let o be an orientation of a 2-dimensional real inner product space V. If the oriented angle between x and y is π/2, then the oriented angle between x and x+y equals arctan( ||y|| / ||x|| ).
Русский
Пусть o — ориентация пространства V размерности 2 с вещественным скалярным произведением. Если угол ориентации между векторами x и y равен π/2, то угол между x и x+y равен arctan( ||y|| / ||x|| ).
LaTeX
$$$ o.oangle x y = \uparrow\left( \frac{\pi}{2} \right) \;\Rightarrow\; o.oangle x (x+y) = \operatorname{Real.Angle.coe}\left( \operatorname{Real.arctan}\left( \frac{\|y\|}{\|x\|} \right) \right) $$$
Lean4
/-- An angle in a right-angled triangle expressed using `arctan`. -/
theorem oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
o.oangle x (x + y) = Real.arctan (‖y‖ / ‖x‖) :=
by
have hs : (o.oangle x (x + y)).sign = 1 := by rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
rw [o.oangle_eq_angle_of_sign_eq_one hs,
InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
(o.left_ne_zero_of_oangle_eq_pi_div_two h)]
