oangle_sub_left_eq_arccos_of_oangle_eq_pi_div_two

English

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

Русский

Если o.oangle x y = π/2, то угол между (y−x) и y равен arctan( ||x|| / ||y|| ).

LaTeX

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

Lean4

/-- An angle in a right-angled triangle expressed using `arccos`, version subtracting vectors. -/
theorem oangle_sub_left_eq_arccos_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle (x - y) x = Real.arccos (‖x‖ / ‖x - y‖) :=
  by
  rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
  exact (-o).oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two h

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