cos_angle_add_of_inner_eq_zero — Mathlib

English

If ⟪x, y⟫ = 0, then cos(angle(x, x + y)) = ||x|| / ||x + y||.

Русский

Если ⟪x, y⟫ = 0, то cos(угол(x, x + y)) = ||x|| / ||x + y||.

LaTeX

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

Lean4

/-- The cosine of an angle in a right-angled triangle as a ratio of sides. -/
theorem cos_angle_add_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) : Real.cos (angle x (x + y)) = ‖x‖ / ‖x + y‖ :=
  by
  rw [angle_add_eq_arccos_of_inner_eq_zero h,
    Real.cos_arccos (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_right (mul_self_nonneg _)

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