inner_lt_one_iff_real_of_norm_one

English

If the inner product of two unit vectors is strictly less than 1, then the vectors are distinct.

Русский

Если скалярное произведение двух единичных векторов строго меньше единицы, тогда векторы различны.

LaTeX

$$$⟪x,y⟫_{\mathbb{R}} < 1 \quad\Rightarrow\quad x \neq y$ для норм единичной длины.$$

Lean4

/-- If the inner product of two unit vectors is strictly less than `1`, then the two vectors are
distinct. One form of the equality case for Cauchy-Schwarz. -/
theorem inner_lt_one_iff_real_of_norm_one {x y : F} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : ⟪x, y⟫_ℝ < 1 ↔ x ≠ y := by
  convert inner_lt_norm_mul_iff_real (F := F) <;> simp [hx, hy]

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