inner_eq_neg_mul_norm_iff_angle_eq_pi

English

Let x,y ≠ 0. The inner product ⟪x,y⟫ equals −‖x‖‖y‖ if and only if the angle between x and y is π.

Русский

Пусть x,y ≠ 0. Скалярное произведение ⟪x,y⟫ равно −‖x‖‖y‖ тогда и только тогда, когда угол между x и y равен π.

LaTeX

$$⟪x,y⟫ = -(‖x‖‖y‖) ↔ angle x y = π (при x ≠ 0 и y ≠ 0)$$

Lean4

/-- The inner product of two non-zero vectors equals the negative product of their norms
if and only if the angle between the two vectors is π. -/
theorem inner_eq_neg_mul_norm_iff_angle_eq_pi {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    ⟪x, y⟫ = -(‖x‖ * ‖y‖) ↔ angle x y = π :=
  by
  refine ⟨fun h => ?_, inner_eq_neg_mul_norm_of_angle_eq_pi⟩
  have h₁ : ‖x‖ * ‖y‖ ≠ 0 := (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy)).ne'
  rw [angle, h, neg_div, div_self h₁, Real.arccos_neg_one]

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