norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two

English

If o.oangle x y = π/2, then ||y|| / tan(o.oangle x (x+y)) = ||x||.

Русский

Если o.oangle x y = π/2, то ||y|| / tan(o.oangle x (x+y)) = ||x||.

LaTeX

$$$ o.oangle x y = \uparrow\left( \frac{\pi}{2} \right) \Rightarrow \frac{\|y\|}{\tan\left(o.oangle x (x+y)\right)} = \|x\| $$$

Lean4

/-- A side of a right-angled triangle divided by the tangent of the opposite angle equals the
adjacent side. -/
theorem norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    ‖y‖ / Real.Angle.tan (o.oangle x (x + 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, Real.Angle.tan_coe,
    InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inr (o.right_ne_zero_of_oangle_eq_pi_div_two h))]

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