English
Let x and y be vectors with ⟪x, y⟫ = 0 and at least one of x, y nonzero. Then angle(x, x + y) = arcsin( ||y|| / ||x + y|| ).
Русский
Пусть x, y — ненулевые по крайней мере по одному из них векторы с ⟪x, y⟫ = 0. Тогда угол между x и x + y равен arcsin( ||y|| / ||x + y|| ).
LaTeX
$$$$ \angle x (x+y) = \arcsin\left( \frac{\|y\|}{\|x+y\|} \right) $$$$
Lean4
/-- An angle in a right-angled triangle expressed using `arcsin`. -/
theorem angle_add_eq_arcsin_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0 ∨ y ≠ 0) :
angle x (x + y) = Real.arcsin (‖y‖ / ‖x + y‖) :=
by
have hxy : ‖x + y‖ ^ 2 ≠ 0 :=
by
rw [pow_two, norm_add_sq_eq_norm_sq_add_norm_sq_real h, ne_comm]
refine ne_of_lt ?_
rcases h0 with (h0 | h0)
· exact Left.add_pos_of_pos_of_nonneg (mul_self_pos.2 (norm_ne_zero_iff.2 h0)) (mul_self_nonneg _)
· exact Left.add_pos_of_nonneg_of_pos (mul_self_nonneg _) (mul_self_pos.2 (norm_ne_zero_iff.2 h0))
rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_eq_arcsin (div_nonneg (norm_nonneg _) (norm_nonneg _)),
div_pow, one_sub_div hxy]
nth_rw 1 [pow_two]
rw [norm_add_sq_eq_norm_sq_add_norm_sq_real h, pow_two, add_sub_cancel_left, ← pow_two, ← div_pow,
Real.sqrt_sq (div_nonneg (norm_nonneg _) (norm_nonneg _))]
