English
Let 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 \neq 0$$$
Lean4
/-- The inner product of two vectors, divided by the product of their
norms, has value 1 if and only if they are nonzero and one is
a positive multiple of the other. -/
theorem real_inner_div_norm_mul_norm_eq_one_iff (x y : F) :
⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1 ↔ x ≠ 0 ∧ ∃ r : ℝ, 0 < r ∧ y = r • x :=
by
constructor
· intro h
have hx₀ : x ≠ 0 := fun h₀ => by simp [h₀] at h
have hy₀ : y ≠ 0 := fun h₀ => by simp [h₀] at h
refine ⟨hx₀, ‖y‖ / ‖x‖, div_pos (norm_pos_iff.2 hy₀) (norm_pos_iff.2 hx₀), ?_⟩
exact ((inner_eq_norm_mul_iff_div hx₀).1 (eq_of_div_eq_one h)).symm
· rintro ⟨hx, ⟨r, ⟨hr, rfl⟩⟩⟩
exact real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul hx hr
