abs_real_inner_div_norm_mul_norm_eq_one_iff

English

For any x,y in a real inner product space, |⟪x,y⟫_ℝ| / (∥x∥ ∥y∥) = 1 iff x ≠ 0 ∧ ∃ r ∈ ℝ, r ≠ 0 ∧ y = r x.

Русский

Для любых x,y в вещественном внутреннем произведении, равенство |⟨x,y⟩| /(∥x∥ ∥y∥) = 1 эквивалентно x ≠ 0 ∧ ∃ r ∈ ℝ, r ≠ 0 ∧ y = r x.

LaTeX

$$$\left|\langle x,y\rangle\right| /(\|x\| \|y\|) = 1 \iff x \neq 0 \land \exists r\in\mathbb{R}, r \neq 0 \land y = r x$$$

Lean4

/-- The inner product of two vectors, divided by the product of their
norms, has absolute value 1 if and only if they are nonzero and one is
a multiple of the other. One form of equality case for Cauchy-Schwarz. -/
theorem abs_real_inner_div_norm_mul_norm_eq_one_iff (x y : F) :
    |⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)| = 1 ↔ x ≠ 0 ∧ ∃ r : ℝ, r ≠ 0 ∧ y = r • x :=
  @norm_inner_div_norm_mul_norm_eq_one_iff ℝ F _ _ _ x y

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