sin_angle_add_of_inner_eq_zero — Mathlib

English

For ⟪x, y⟫ = 0, cos(angle(x, x + y)) · ||x + y|| = ||x||.

Русский

Для ⟪x, y⟫ = 0 верно: cos(angle(x, x + y)) · ||x + y|| = ||x||.

LaTeX

$$$$ \cos\big( \angle x (x+y) \big) \cdot \|x+y\| = \|x\| $$$$

Lean4

/-- The sine of an angle in a right-angled triangle as a ratio of sides. -/
theorem sin_angle_add_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0 ∨ y ≠ 0) :
    Real.sin (angle x (x + y)) = ‖y‖ / ‖x + y‖ :=
  by
  rw [angle_add_eq_arcsin_of_inner_eq_zero h h0,
    Real.sin_arcsin (le_trans (by simp) (div_nonneg (norm_nonneg _) (norm_nonneg _)))
      (div_le_one_of_le₀ _ (norm_nonneg _))]
  rw [mul_self_le_mul_self_iff (norm_nonneg _) (norm_nonneg _), norm_add_sq_eq_norm_sq_add_norm_sq_real h]
  exact le_add_of_nonneg_left (mul_self_nonneg _)

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