# Rays in a real normed vector space #

In this file we prove some lemmas about the `SameRay` 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`.

source
theorem SameRay.norm_add {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x y : E} (h : SameRay ℝ x y) :
‖x + y‖ = ‖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.

source
theorem SameRay.norm_sub {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x y : E} (h : SameRay ℝ x y) :
‖x - y‖ = |‖x‖ - ‖y‖|
source
theorem SameRay.norm_smul_eq {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {x y : E} (h : SameRay ℝ x y) :
‖x‖ • y = ‖y‖ • x
source
theorem norm_injOn_ray_left {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {x : F} (hx : x ≠ 0) :
Set.InjOn norm {y : F | SameRay ℝ x y}
source
theorem norm_injOn_ray_right {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {y : F} (hy : y ≠ 0) :
Set.InjOn norm {x : F | SameRay ℝ x y}
source
theorem sameRay_iff_norm_smul_eq {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {x y : F} :
SameRay ℝ x y ↔ ‖x‖ • y = ‖y‖ • x
source
theorem sameRay_iff_inv_norm_smul_eq_of_ne {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {x y : F} (hx : x ≠ 0) (hy : y ≠ 0) :
SameRay ℝ x y ↔ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

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.

source
theorem SameRay.inv_norm_smul_eq {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {x y : F} (hx : x ≠ 0) (hy : y ≠ 0) :
SameRay ℝ x y → ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Alias of the forward direction of `sameRay_iff_inv_norm_smul_eq_of_ne`.

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.

source
theorem sameRay_iff_inv_norm_smul_eq {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {x y : F} :
SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

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.

source
theorem sameRay_iff_of_norm_eq {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {x y : F} (h : ‖x‖ = ‖y‖) :
SameRay ℝ x y ↔ x = y

Two vectors of the same norm are on the same ray if and only if they are equal.

source
theorem not_sameRay_iff_of_norm_eq {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {x y : F} (h : ‖x‖ = ‖y‖) :
¬SameRay ℝ x y ↔ x ≠ y
source
theorem SameRay.eq_of_norm_eq {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {x y : F} (h : SameRay ℝ x y) (hn : ‖x‖ = ‖y‖) :
x = y

If two points on the same ray have the same norm, then they are equal.

source
theorem SameRay.norm_eq_iff {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {x y : F} (h : SameRay ℝ x y) :
‖x‖ = ‖y‖ ↔ x = y

The norms of two vectors on the same ray are equal if and only if they are equal.