# mathlibdocumentation

analysis.normed_space.ray

# 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.

theorem same_ray.norm_add {E : Type u_1} [ E] {x y : E} (h : 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.

theorem same_ray.norm_sub {E : Type u_1} [ E] {x y : E} (h : y) :
theorem same_ray.norm_smul_eq {E : Type u_1} [ E] {x y : E} (h : y) :
theorem norm_inj_on_ray_left {F : Type u_2} [normed_group F] [ F] {x : F} (hx : x 0) :
{y : F | y}
theorem norm_inj_on_ray_right {F : Type u_2} [normed_group F] [ F] {y : F} (hy : y 0) :
{x : F | y}
theorem same_ray_iff_norm_smul_eq {F : Type u_2} [normed_group F] [ F] {x y : F} :
theorem same_ray_iff_inv_norm_smul_eq_of_ne {F : Type u_2} [normed_group F] [ F] {x y : F} (hx : x 0) (hy : y 0) :

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.

theorem same_ray.inv_norm_smul_eq {F : Type u_2} [normed_group F] [ F] {x y : F} (hx : x 0) (hy : y 0) :

Alias of the forward direction of same_ray_iff_inv_norm_smul_eq_of_ne.

theorem same_ray_iff_inv_norm_smul_eq {F : Type u_2} [normed_group F] [ F] {x y : F} :

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.

theorem same_ray_iff_of_norm_eq {F : Type u_2} [normed_group F] [ F] {x y : F} (h : x = y) :
y x = y
theorem not_same_ray_iff_of_norm_eq {F : Type u_2} [normed_group F] [ F] {x y : F} (h : x = y) :
¬ y x y