English
For any vectors x,y, equality ∥x+y∥ = ∥x∥ + ∥y∥ occurs exactly when y is a nonnegative multiple of x, i.e. ∥y∥ x = ∥x∥ y.
Русский
Для любых векторов x,y равенство ∥x+y∥ = ∥x∥ + ∥y∥ выполняется тогда, когда y — неотрицательный кратный x, т.е. ∥y∥ x = ∥x∥ y.
LaTeX
$$$\|x+y\| = \|x\| + \|y\| \iff \|y\| \cdot x = \|x\| \cdot y$$$
Lean4
/-- Equality is achieved in the triangle inequality iff the two vectors are collinear. -/
theorem norm_add_eq_iff_real {x y : F} : ‖x + y‖ = ‖x‖ + ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y := by
rw [← pow_left_inj₀ (norm_nonneg _) (Left.add_nonneg (norm_nonneg _) (norm_nonneg _)) two_ne_zero,
norm_add_sq (𝕜 := ℝ), add_pow_two, add_left_inj, add_right_inj, re_to_real, mul_assoc, mul_right_inj' two_ne_zero, ←
inner_eq_norm_mul_iff_real]
