English
If x and y lie on the same ray, then the norm of their sum equals the sum of their norms.
Русский
Если векторы x и y лежат на одном луче, то их сумма имеет норму, равную сумме норм.
LaTeX
$$$$ \text{If } \text{SameRay}(\mathbb{R},x,y) \text{ then } \|x+y\| = \|x\| + \|y\|. $$$$
Lean4
/-- If `x` and `y` are on the same ray, then the triangle inequality becomes the equality: the norm
of `x + y` is the sum of the norms of `x` and `y`. The converse is true for a strictly convex
space. -/
theorem norm_add (h : SameRay ℝ x y) : ‖x + y‖ = ‖x‖ + ‖y‖ :=
by
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
rw [← add_smul, norm_smul_of_nonneg (add_nonneg ha hb), norm_smul_of_nonneg ha, norm_smul_of_nonneg hb, add_mul]
