sin_angle_add_mul_norm_of_inner_eq_zero

English

If ⟪x, y⟫ = 0 and at least one of x,y nonzero, then sin(angle(x, x + y)) = ||y|| / ||x + y||.

Русский

Если ⟪x, y⟫ = 0 и хотя бы один из x,y не нулевой, то sin(угол(x, x+y)) = ||y|| / ||x+y||.

LaTeX

$$$$ \sin\big( \angle x (x+y) \big) = \frac{\|y\|}{\|x+y\|} $$$$

Lean4

/-- The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
opposite side. -/
theorem sin_angle_add_mul_norm_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) :
    Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖ :=
  by
  by_cases h0 : x = 0 ∧ y = 0; · simp [h0]
  rw [not_and_or] at h0
  rw [sin_angle_add_of_inner_eq_zero h h0, div_mul_cancel₀]
  rw [← mul_self_ne_zero, norm_add_sq_eq_norm_sq_add_norm_sq_real h]
  refine (ne_of_lt ?_).symm
  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))

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