norm_sub_eq_add_norm_of_angle_eq_pi

English

If the angle between x and y is π, then ‖x − y‖ = ‖x‖ + ‖y‖.

Русский

Если угол между x и y равен π, то ‖x − y‖ = ‖x‖ + ‖y‖.

LaTeX

$$$\\angle x y = \\pi \\;\\rightarrow\\; \\|x - y\\| = \\|x\\| + \\|y\\|$$$

Lean4

/-- If the angle between two vectors is π, the norm of their difference equals
the sum of their norms. -/
theorem norm_sub_eq_add_norm_of_angle_eq_pi {x y : V} (h : angle x y = π) : ‖x - y‖ = ‖x‖ + ‖y‖ :=
  by
  rw [← sq_eq_sq₀ (norm_nonneg (x - y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)), norm_sub_pow_two_real,
    inner_eq_neg_mul_norm_of_angle_eq_pi h]
  ring

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