norm_add_eq_add_norm_of_angle_eq_zero

English

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

Русский

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

LaTeX

$$angle x y = 0 → ‖x + y‖ = ‖x‖ + ‖y‖$$

Lean4

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

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