SameRay.eq_of_norm_eq
theorem SameRay.eq_of_norm_eq :
∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x y : F},
SameRay ℝ x y → ‖x‖ = ‖y‖ → x = y
The theorem states that in a real normed space, if two points are on the same ray and they have the same norm, then they must be equal. Here, a "ray" is defined such that two vectors are on the same ray if either one is zero or they are positive multiples of each other. The norm is a measure of the "length" or "size" of the vectors, typically defined on vector spaces. The theorem essentially says that no two distinct points on the same ray in a real normed space can have the same length from the origin.
More concisely: In a real normed space, two vectors on the same ray have equal norms if and only if they are equal.
|
SameRay.inv_norm_smul_eq
theorem SameRay.inv_norm_smul_eq :
∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x y : F},
x ≠ 0 → y ≠ 0 → SameRay ℝ x y → ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
The theorem `SameRay.inv_norm_smul_eq` states that for any two non-zero vectors `x` and `y` in a real normed space, they are on the same ray (according to the definition of `SameRay`, meaning either one of them is zero or some positive multiples of them are equal) if and only if the unit vectors obtained by scaling `x` and `y` by the inverse of their norms are equal. In mathematical terms, if $x, y \neq 0$ and $x, y$ are in the same ray, then $\frac{1}{\|x\|}x = \frac{1}{\|y\|}y$.
More concisely: For any non-zero vectors x and y in a real normed space, they are on the same ray if and only if their unit vectors obtained by scaling by the inverse of their norms are equal. That is, $\frac{1}{\|x\|}x = \frac{1}{\|y\|}y$.
|
sameRay_iff_of_norm_eq
theorem sameRay_iff_of_norm_eq :
∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x y : F},
‖x‖ = ‖y‖ → (SameRay ℝ x y ↔ x = y)
The theorem `sameRay_iff_of_norm_eq` states that for any normed vector space over the real numbers, if two vectors have the same norm, then they are in the same ray if and only if they are equal. Here, vectors being on the same ray is defined as either one of the vectors being zero or there existing positive multiples of the vectors such that they are equal. In simpler terms, this theorem says if two vectors have the same length, then they point in the same direction (or opposite directions) if and only if they are exactly the same vector.
More concisely: In a real normed vector space, two vectors have the same norm if and only if they are equal or lie on the same ray.
|
sameRay_iff_inv_norm_smul_eq
theorem sameRay_iff_inv_norm_smul_eq :
∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x y : F},
SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
Two vectors `x` and `y` in a real normed space are on the same ray if and only if one of them is zero or the unit vectors obtained by scaling `x` and `y` each by the reciprocal of its norm are equal. In other words, `x` and `y` are on the same ray if either `x` is zero, `y` is zero, or `‖x‖⁻¹ • x = ‖y‖⁻¹ • y`, where `‖x‖` and `‖y‖` are the norms of `x` and `y` respectively, and `•` represents vector scaling.
More concisely: Two vectors in a real normed space are on the same ray if and only if they are scalar multiples of each other, where the scalars are the reciprocals of their respective norms.
|
SameRay.norm_eq_iff
theorem SameRay.norm_eq_iff :
∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x y : F},
SameRay ℝ x y → (‖x‖ = ‖y‖ ↔ x = y)
The theorem states that for any two vectors `x` and `y` in a normed space over the real numbers, if `x` and `y` are on the same ray, then the norms of `x` and `y` are equal if and only if `x` and `y` are equal. Here, two vectors are considered on the same ray if either one of them is zero, or some positive multiples of them are equal. The norm, denoted as `‖x‖` or `‖y‖`, refers to the length or magnitude of the vector in the normed space.
More concisely: In a normed space over the real numbers, two non-zero vectors have equal norms if and only if they are collinear and one is a scalar multiple of the other.
|
sameRay_iff_inv_norm_smul_eq_of_ne
theorem sameRay_iff_inv_norm_smul_eq_of_ne :
∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x y : F},
x ≠ 0 → y ≠ 0 → (SameRay ℝ x y ↔ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y)
This theorem states that for any two non-zero vectors `x` and `y` in a real normed space, these vectors are on the same ray if and only if their unit vectors, obtained by scaling the vectors by the inverse of their norms (`‖x‖⁻¹ • x` and `‖y‖⁻¹ • y`), are equal. In mathematical terms, we can say: for all non-zero `x` and `y` in a real normed space, `x` and `y` are on the same ray if and only if the vectors `x/‖x‖` and `y/‖y‖` are equal.
More concisely: For any two non-zero vectors in a real normed space, they are on the same ray if and only if their corresponding unit vectors are equal.
|
SameRay.norm_add
theorem SameRay.norm_add :
∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x y : E},
SameRay ℝ x y → ‖x + y‖ = ‖x‖ + ‖y‖
This theorem states that if two vectors `x` and `y` in a semi-normed additive commutative group that also has a normed space over the real numbers are on the same ray (that is, one of them is zero or some positive multiples of them are equal), then the norm of the sum of `x` and `y` is equal to the sum of the norms of `x` and `y`. Furthermore, the converse of this statement is true if the space is strictly convex.
More concisely: If `x` and `y` are vectors in a real semi-normed additive commutative group that is also a normed space, and they lie on the same ray, then the norm of their sum is equal to the sum of their norms; conversely, this holds if the space is strictly convex.
|