norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two

English

If o.oangle x y = π/2, then the norm of y divided by the sine of o.oangle(x−y, x) equals the norm of x−y.

Русский

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

LaTeX

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

Lean4

/-- A side of a right-angled triangle divided by the sine of the opposite angle equals the
hypotenuse, version subtracting vectors. -/
theorem norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    ‖x‖ / Real.Angle.sin (o.oangle y (y - x)) = ‖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.sin_coe,
    InnerProductGeometry.norm_div_sin_angle_sub_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inr (o.left_ne_zero_of_oangle_eq_pi_div_two h))]

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