oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two

English

In a right-angled 2D arrangement, adding x to y on the left yields an angle equal to arcsin of a ratio: ‖y‖/‖x+y‖.

Русский

В правой системе 2D добавление x слева даёт угол, равный arcsin(‖y‖/‖x+y‖).

LaTeX

$$$\\forall x,y\\in V,\\ o.oangle(x,y) = \\arcsin\\left(\\frac{\\|y\\|}{\\|x+y\\|}\\right) \\text{ under appropriate conditions}.$$$

Lean4

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

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