oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two

English

If o.oangle x y = π/2, then o.oangle y (y−x) = arccos( ||y|| / ||y−x|| ).

Русский

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

LaTeX

$$$ o.oangle x y = \uparrow\left( \frac{\pi}{2} \right) \Rightarrow o.oangle y (y-x) = \operatorname{Real.Angle.coe}\left( \operatorname{Real.arccos}\left( \frac{\|y\|}{\|y-x\|} \right) \right) $$$

Lean4

/-- An angle in a right-angled triangle expressed using `arccos`, version subtracting vectors. -/
theorem oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle y (y - x) = Real.arccos (‖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,
    InnerProductGeometry.angle_sub_eq_arccos_of_inner_eq_zero (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)]

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