angle_add_eq_arctan_of_inner_eq_zero

English

Let x and y be vectors with ⟪x, y⟫ = 0 and x ≠ 0. Then angle(x, x + y) = arctan( ||y|| / ||x|| ).

Русский

Пусть x и y векторы с ⟪x, y⟫ = 0 и x ≠ 0. Тогда угол между x и x + y равен arctan( ||y|| / ||x|| ).

LaTeX

$$$$ \angle x (x+y) = \arctan\left( \frac{\|y\|}{\|x\|} \right) $$$$

Lean4

/-- An angle in a right-angled triangle expressed using `arctan`. -/
theorem angle_add_eq_arctan_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0) :
    angle x (x + y) = Real.arctan (‖y‖ / ‖x‖) :=
  by
  rw [angle_add_eq_arcsin_of_inner_eq_zero h (Or.inl h0), Real.arctan_eq_arcsin, ← div_mul_eq_div_div,
    norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]
  nth_rw 3 [← Real.sqrt_sq (norm_nonneg x)]
  rw_mod_cast [← Real.sqrt_mul (sq_nonneg _), div_pow, pow_two, pow_two, mul_add, mul_one, mul_div,
    mul_comm (‖x‖ * ‖x‖), ← mul_div, div_self (mul_self_pos.2 (norm_ne_zero_iff.2 h0)).ne', mul_one]

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