norm_sub_eq_add_norm_iff_angle_eq_pi

English

For nonzero x,y, ‖x − y‖ = ‖x‖ + ‖y‖ if and only if angle x y = π.

Русский

Для ненулевых x,y: ‖x − y‖ = ‖x‖ + ‖y‖ тогда и только тогда, когда угол x y равен π.

LaTeX

$$‖x − y‖ = ‖x‖ + ‖y‖ ↔ angle x y = π (для x ≠ 0, y ≠ 0)$$

Lean4

/-- The norm of the difference of two non-zero vectors equals the sum of their norms
if and only the angle between the two vectors is π. -/
theorem norm_sub_eq_add_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 => ?_, norm_sub_eq_add_norm_of_angle_eq_pi⟩
  rw [← inner_eq_neg_mul_norm_iff_angle_eq_pi hx hy]
  obtain ⟨hxy₁, hxy₂⟩ := norm_nonneg (x - y), add_nonneg (norm_nonneg x) (norm_nonneg y)
  rw [← sq_eq_sq₀ hxy₁ hxy₂, norm_sub_pow_two_real] at h
  calc
    ⟪x, y⟫ = (‖x‖ ^ 2 + ‖y‖ ^ 2 - (‖x‖ + ‖y‖) ^ 2) / 2 := by linarith
    _ = -(‖x‖ * ‖y‖) := by ring

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