oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two

English

If o.oangle x y equals π/2, then o.oangle (x + y) y equals arccos of a ratio of norms: ‖y‖ / ‖x+y‖.

Русский

Если угол o.oangle x y равен π/2, то угол o.oangle (x+y) y равен arccos(‖y‖ / ‖x+y‖).

LaTeX

$$$\\text{If } o.oangle(x,y)=\\pi/2, \\text{ then } o.oangle(x+y,y)=\\arccos\\left(\\frac{\\|y\\|}{\\|x+y\\|}\\right).$$$

Lean4

/-- An angle in a right-angled triangle expressed using `arccos`. -/
theorem oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle x (x + y) = Real.arccos (‖x‖ / ‖x + y‖) :=
  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_arccos_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]

Похожие утверждения