cos_oangle_add_right_of_oangle_eq_pi_div_two

English

If the angle between x and y is π/2, then cos of the angle between x and x+y equals ||x|| / ||x+y||.

Русский

Если угол между x и y равен π/2, то косинус угла между x и x+y равен ||x|| / ||x+y||.

LaTeX

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

Lean4

/-- The cosine of an angle in a right-angled triangle as a ratio of sides. -/
theorem cos_oangle_add_right_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.cos (o.oangle x (x + y)) = ‖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, Real.Angle.cos_coe,
    InnerProductGeometry.cos_angle_add_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]

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