real_inner_div_norm_mul_norm_eq_neg_one_iff

English

For x,y ∈ E, ⟪x,y⟫ = ‖x‖ ‖y‖ holds if and only if y is a nonnegative real multiple of x, i.e. y = t x with t ≥ 0.

Русский

Для векторов x,y верно ⟪x,y⟫ = ‖x‖‖y‖ тогда и только тогда, когда y = t x для некоторого t ≥ 0.

LaTeX

$$$⟪x,y⟫ = ∥x∥ ∥y∥ \iff y = t x\text{ for some }t \ge 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 negative multiple of the other. -/
theorem real_inner_div_norm_mul_norm_eq_neg_one_iff (x y : F) :
    ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = -1 ↔ x ≠ 0 ∧ ∃ r : ℝ, r < 0 ∧ y = r • x :=
  by
  rw [← neg_eq_iff_eq_neg, ← neg_div, ← inner_neg_right, ← norm_neg y, real_inner_div_norm_mul_norm_eq_one_iff,
    (@neg_surjective ℝ _).exists]
  refine Iff.rfl.and (exists_congr fun r => ?_)
  rw [neg_pos, neg_smul, neg_inj]

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