Rays in a real normed vector space #
In this file we prove some lemmas about the same_ray
predicate in case of a real normed space. In
this case, for two vectors x y
in the same ray, the norm of their sum is equal to the sum of their
norms and ∥y∥ • x = ∥x∥ • y
.
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.
Two nonzero vectors x y
in a real normed space are on the same ray if and only if the unit
vectors ∥x∥⁻¹ • x
and ∥y∥⁻¹ • y
are equal.
Alias of the forward direction of same_ray_iff_inv_norm_smul_eq_of_ne
.
Two vectors x y
in a real normed space are on the ray if and only if one of them is zero or
the unit vectors ∥x∥⁻¹ • x
and ∥y∥⁻¹ • y
are equal.
Two vectors of the same norm are on the same ray if and only if they are equal.
If two points on the same ray have the same norm, then they are equal.
The norms of two vectors on the same ray are equal if and only if they are equal.