Documentation

Mathlib.Analysis.NormedSpace.Ray

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.

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

theorem SameRay.norm_sub {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace E] {x : E} {y : E} (h : SameRay x y) :
theorem SameRay.norm_smul_eq {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace E] {x : E} {y : E} (h : SameRay x y) :
theorem norm_injOn_ray_left {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {x : F} (hx : x 0) :
Set.InjOn norm {y | SameRay x y}
theorem norm_injOn_ray_right {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {y : F} (hy : y 0) :
Set.InjOn norm {x | SameRay x y}
theorem sameRay_iff_inv_norm_smul_eq_of_ne {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {x : F} {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 SameRay.inv_norm_smul_eq {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {x : F} {y : F} (hx : x 0) (hy : y 0) :

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.

theorem sameRay_iff_inv_norm_smul_eq {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {x : F} {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 sameRay_iff_of_norm_eq {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {x : F} {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.

theorem not_sameRay_iff_of_norm_eq {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {x : F} {y : F} (h : x = y) :
theorem SameRay.eq_of_norm_eq {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {x : F} {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.

theorem SameRay.norm_eq_iff {F : Type u_2} [NormedAddCommGroup F] [NormedSpace F] {x : F} {y : F} (h : SameRay x y) :

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