real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul

English

If x ≠ 0 and r < 0, then ⟪x, r·x⟫ℝ / (∥x∥ ∥r·x∥) = -1.

Русский

Если x ≠ 0 и r < 0, тогда ⟪x, r·x⟫ℝ / (∥x∥ ∥r·x∥) = -1.

LaTeX

$$$\frac{\langle x, r\cdot x\rangle_{\mathbb{R}}}{\|x\| \|r\cdot x\|} = -1$ при $x\neq 0$, $r<0$$$

Lean4

/-- The inner product of a nonzero vector with a negative multiple of
itself, divided by the product of their norms, has value -1. -/
theorem real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul {x : F} {r : ℝ} (hx : x ≠ 0) (hr : r < 0) :
    ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = -1 :=
  by
  rw [real_inner_smul_self_right, norm_smul, Real.norm_eq_abs, ← mul_assoc ‖x‖, mul_comm _ |r|, mul_assoc,
    abs_of_neg hr, neg_mul, div_neg_eq_neg_div, div_self]
  exact mul_ne_zero hr.ne (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))

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