cos_oangle_sub_right_of_oangle_eq_pi_div_two

English

If the oriented angle between x and y is π/2, then the cosine of the oriented angle between y and y−x equals the ratio ||y||/||y−x||.

Русский

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

LaTeX

$$$ \cos(o.oangle(y, y - x)) = \frac{\|y\|}{\|y - x\|} $$$

Lean4

/-- The cosine of an angle in a right-angled triangle as a ratio of sides, version subtracting
vectors. -/
theorem cos_oangle_sub_right_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.cos (o.oangle y (y - x)) = ‖y‖ / ‖y - x‖ :=
  by
  have hs : (o.oangle y (y - x)).sign = 1 := by rw [oangle_sign_sub_right_swap, 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_sub_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)]

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