Orientation.oangle_sub_left
theorem Orientation.oangle_sub_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y z : V},
x ≠ 0 → y ≠ 0 → z ≠ 0 → o.oangle x z - o.oangle x y = o.oangle y z
The theorem `Orientation.oangle_sub_left` states that for a real inner product space `V` of finite dimension 2, given an orientation `o` of `V` and any three nonzero vectors `x`, `y`, and `z` from `V`, the difference between the angle (`o.oangle`) between vector `x` and vector `z` and the angle between vector `x` and vector `y` is equal to the angle between vector `y` and vector `z`. In mathematical terms, this can be written as: $\angle xz - \angle xy = \angle yz$.
More concisely: For any real inner product space of dimension 2 with orientation `o`, the difference between the angles between vectors `x`, `z`, and `x`, `y` is equal to the angle between `y` and `z`, i.e., $\angle xz - \angle xy = \angle yz$.
|
Orientation.oangle_eq_pi_iff_sameRay_neg
theorem Orientation.oangle_eq_pi_iff_sameRay_neg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑Real.pi ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)
The theorem `Orientation.oangle_eq_pi_iff_sameRay_neg` states that for a 2-dimensional real inner product space `V`, the oriented angle between two vectors `x` and `y` is π if and only if both vectors are nonzero and the first vector `x` lies on the same ray as the negation of the second vector `y`. Here, the oriented angle is defined with respect to a given orientation `o` of the space `V`. The concept of "same ray" means that either one of the vectors is zero, or some positive multiples of them are equal, typically implying that one vector is a nonnegative multiple of the other.
More concisely: For a 2-dimensional real inner product space with a given orientation, the oriented angle between vectors x and y is π if and only if x and -y lie on the same ray.
|
Orientation.ne_of_oangle_eq_pi_div_two
theorem Orientation.ne_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → x ≠ y
The theorem `Orientation.ne_of_oangle_eq_pi_div_two` states that given a real valued inner product space `V` of finite rank 2 and an orientation of `V`, if the angle between two vectors `x` and `y` in `V` is `π / 2`, then the vectors `x` and `y` are not equal.
More concisely: If two vectors in a finite-rank 2 real inner product space have an angle equal to π/2 with respect to a given orientation, then they are not equal.
|
Orientation.oangle_eq_zero_iff_oangle_rev_eq_zero
theorem Orientation.oangle_eq_zero_iff_oangle_rev_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = 0 ↔ o.oangle y x = 0
This theorem, "Orientation.oangle_eq_zero_iff_oangle_rev_eq_zero", asserts that for any 2-dimensional real inner product space `V` with a specified orientation `o`, and any two vectors `x` and `y` in this space, the oriented angle `o.oangle` between `x` and `y` is zero if and only if the oriented angle between `y` and `x` is zero. In other words, the orientation of the angle between two vectors is unaffected by the order of the vectors.
More concisely: For any 2-dimensional real inner product space with orientation and vectors x, y, the oriented angle between x and y is equal to the negated oriented angle between y and x.
|
Orientation.oangle_eq_pi_iff_oangle_rev_eq_pi
theorem Orientation.oangle_eq_pi_iff_oangle_rev_eq_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑Real.pi ↔ o.oangle y x = ↑Real.pi
This theorem is stating that for a normed additive group over a real inner product space of dimension 2, the oriented angle between two vectors is equal to π if and only if the angle between the vectors when their positions are swapped is also equal to π. In other words, if we have an orientation of the space and two vectors in that space, the directed angle from the first to the second vector being π implies the directed angle from the second to the first vector is also π, and vice versa.
More concisely: For vectors in a 2-dimensional real inner product space with fixed orientation, the oriented angles between them are equal if and only if they are oppositely directed right angles.
|
Orientation.oangle_ne_zero_and_ne_pi_iff_linearIndependent
theorem Orientation.oangle_ne_zero_and_ne_pi_iff_linearIndependent :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y ≠ 0 ∧ o.oangle x y ≠ ↑Real.pi ↔ LinearIndependent ℝ ![x, y]
The theorem `Orientation.oangle_ne_zero_and_ne_pi_iff_linearIndependent` states that for a 2-dimensional real inner product space `V` with a given orientation `o`, two vectors `x` and `y` are linearly independent if and only if the oriented angle between `x` and `y` is neither zero nor `π`. In other words, if `x` and `y` are not linear dependent (i.e., one can't be expressed as a scalar multiple of the other), then the angle between them isn't zero or `π`. Conversely, if the angle between `x` and `y` isn't zero or `π`, then `x` and `y` aren't linearly dependent.
More concisely: In a 2-dimensional real inner product space with a given orientation, two vectors are linearly independent if and only if their oriented angle is neither 0 nor π.
|
Orientation.oangle_add_oangle_rev_neg_left
theorem Orientation.oangle_add_oangle_rev_neg_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
o.oangle (-x) y + o.oangle (-y) x = 0
This theorem states that for a real inner product space of two-dimensional vectors, given any orientation of the space and two vectors 'x' and 'y', the sum of the angles between the negation of vector 'x' and vector 'y', and the negation of vector 'y' and vector 'x', is always zero. Here, 'o.oangle (-x) y' and 'o.oangle (-y) x' represent the oriented angles from '-x' to 'y' and from '-y' to 'x' respectively, according to the given orientation 'o'.
More concisely: For any orientation in a two-dimensional real inner product space, the sum of the oriented angles between the negation of vector x and vector y, and the negation of vector y and vector x, is zero.
|
Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq
theorem Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
x ≠ y → ‖x‖ = ‖y‖ → o.oangle y x = ↑Real.pi - 2 • o.oangle (y - x) y
This theorem, named `Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq`, states that given a real inner product space V of finite dimension 2 and a certain orientation of V, for any two distinct vectors x and y in V of the same norm, the oriented angle between y and x equals pi minus twice the oriented angle between y-x and y. Here, "oriented angle" refers to the angle measure that respects the chosen orientation of the vector space, and "pi" is the constant 3.14159265... . The theorem can be thought of as a generalization of the geometric fact about isosceles triangles, where the angle at the apex equals pi minus twice a base angle.
More concisely: For any 2-dimensional real inner product space V with a fixed orientation, the oriented angle between two vectors x and y of the same norm is equal to pi - 2 * the oriented angle between y - x and y.
|
Orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq
theorem Orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
‖x‖ = ‖y‖ → o.oangle x (x - y) = o.oangle (y - x) y
The theorem `Orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq` is a form of the Pons Asinorum (Bridge of asses), specifically the oriented vector angle form, in the context of real inner product spaces. The theorem states that for any real vector space `V` endowed with normed add comm group structure, inner product space over reals, and is of finite dimension equal to 2, any orientation `o` of this vector space, and vectors `x` and `y` in `V` such that the norm of `x` equals the norm of `y`, the oriented angle between `x` and the vector resulting from `x` subtract `y` is equal to the oriented angle between the vector resulting from `y` subtract `x` and `y`. The name "Pons Asinorum" refers to a statement that is easy to understand once learned but difficult to master, reminiscent of Euclid's fifth postulate in geometry.
More concisely: For any 2-dimensional real inner product space endowed with a normed additive commutative group structure, and for any vectors x and y with equal norms, the oriented angle between x and y is equal to the oriented angle between y and (x - y).
|
Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent
theorem Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = 0 ∨ o.oangle x y = ↑Real.pi ↔ ¬LinearIndependent ℝ ![x, y]
This theorem states that for a 2-dimensional real inner product space `V` with a given orientation `o`, the oriented angle between two vectors `x` and `y` in `V` is either 0 or π if and only if the vectors `x` and `y` are not linearly independent. In other words, if `x` and `y` are linearly dependent, then the oriented angle between them with respect to the orientation `o` must be either 0 or π. Conversely, if the oriented angle between `x` and `y` is 0 or π, then `x` and `y` must be linearly dependent.
More concisely: In a 2-dimensional real inner product space with a given orientation, two non-zero vectors are linearly dependent if and only if their oriented angle is 0 or π.
|
Orientation.eq_iff_norm_eq_of_oangle_eq_zero
theorem Orientation.eq_iff_norm_eq_of_oangle_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = 0 → (x = y ↔ ‖x‖ = ‖y‖)
The theorem `Orientation.eq_iff_norm_eq_of_oangle_eq_zero` states that for any two vectors `x` and `y` in a real, 2-dimensional inner product space `V` with a given orientation `o`, if the oriented angle `o.oangle x y` between `x` and `y` is zero, then `x` equals `y` if and only if the norm of `x` (denoted by `‖x‖`) equals the norm of `y` (denoted by `‖y‖`). Here, the orientation of a module refers to the direction in which we consider angles to increase, and the oriented angle between two vectors is an angle that takes this orientation into account.
More concisely: In a real, 2-dimensional inner product space with a fixed orientation, two vectors have equal norms if and only if their oriented angle between them is zero.
|
Orientation.right_ne_zero_of_oangle_eq_pi
theorem Orientation.right_ne_zero_of_oangle_eq_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑Real.pi → y ≠ 0
This theorem states that in a real inner product space of rank 2, if the angle between two vectors is `π` radians (which corresponds to 180 degrees), then the second vector cannot be the zero vector. This is useful for proving properties related to vector orientation and angles in two-dimensional spaces.
More concisely: In a real inner product space of rank 2, two vectors with an angle of π radians between them are linearly independent.
|
Orientation.two_zsmul_oangle_neg_self_right
theorem Orientation.two_zsmul_oangle_neg_self_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V),
2 • o.oangle x (-x) = 0
The theorem named `Orientation.two_zsmul_oangle_neg_self_right` states that for any normed additive commutative group `V` equipped with an inner product space over the real numbers, and for any orientation `o` of `V` (when the rank of `V` as a module over ℝ is 2), the angle between any vector `x` in `V` and its negation multiplied by 2 equals zero. This essentially formalizes the geometrical intuition that the angle between a vector and its negation in a two-dimensional real vector space is half a full rotation, or equivalently, 180 degrees or $\pi$ radians, and thus its double is a full rotation, or equivalently, 360 degrees or $2\pi$ radians, which is equivalent to 0 in the context of angles.
More concisely: In a 2-dimensional real inner product space, the angle between a vector and its negation is equal to 0.
|
Orientation.oangle_smul_left_self_of_nonneg
theorem Orientation.oangle_smul_left_self_of_nonneg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) {r : ℝ},
0 ≤ r → o.oangle (r • x) x = 0
This theorem states that the angle between a nonnegative multiple of a vector and the vector itself is 0. To be precise, given a vector space `V` that is a normed add commutative group and an inner product space over the reals with finite dimension 2, an orientation `o` of `V`, a vector `x` in `V`, and a nonnegative real number `r`, the orientation angle between `r` times `x` and `x` is 0. This essentially means that a vector and its nonnegative multiples lie on the same line in our two-dimensional space.
More concisely: The angle between a vector and a nonnegative scalar multiple of that vector is zero in a two-dimensional inner product space.
|
Orientation.left_ne_zero_of_oangle_sign_ne_zero
theorem Orientation.left_ne_zero_of_oangle_sign_ne_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
(o.oangle x y).sign ≠ 0 → x ≠ 0
This theorem states that in a 2-dimensional real inner product space (a normed additive commutative group with a real inner product), if the signed angle (as determined by a given orientation) between two vectors is non-zero, then the first vector must be non-zero. This essentially says that a non-zero angle implies that the vectors making that angle must be non-zero themselves.
More concisely: In a 2-dimensional real inner product space, if the angle between two non-zero vectors is non-zero, then both vectors are non-zero.
|
Orientation.oangle_sign_sub_smul_left
theorem Orientation.oangle_sign_sub_smul_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) (r : ℝ),
(o.oangle (x - r • y) y).sign = (o.oangle x y).sign
This theorem states that for a real inner product space `V` of finite rank 2, given an orientation `o` of this space and two vectors `x`, `y` in `V`, along with a real number `r`, the sign of the angle formed by the vector `x - r • y` and `y` under the orientation `o` is the same as the sign of the angle formed by `x` and `y` under the same orientation. In other words, subtracting a multiple of the second vector from the first one does not change the sign of the angle between the two vectors under a given orientation.
More concisely: For a real inner product space of finite rank 2 with orientation, the sign of the angle between vector `x` and `y` under orientation is equal to the sign of the angle between `x - r*y` and `y` under the same orientation, for any vectors `x, y` and scalar `r`.
|
Orientation.oangle_zero_left
theorem Orientation.oangle_zero_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V), o.oangle 0 x = 0
This theorem states that in a real inner product space `V`, which is a normed add commutative group with an orientation (a module structure) and is known to have a finite dimension of 2, if the first vector passed to the `oangle` function (which presumably computes the oriented angle between two vectors) is 0, then the output of the function will be 0, for any given second vector `x`. This is consistent with the intuitive geometric notion that the angle between the zero vector and any other vector is undefined, and here it is conventionally set to 0.
More concisely: In a 2-dimensional real inner product space, the oriented angle between the zero vector and any vector is conventionally defined as 0.
|
Orientation.ne_of_oangle_sign_ne_zero
theorem Orientation.ne_of_oangle_sign_ne_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
(o.oangle x y).sign ≠ 0 → x ≠ y
This theorem states that in a 2-dimensional real inner product space, if the sign of the oriented angle between two vectors is nonzero, then the two vectors are not equal. In other words, in such a space, the only way two vectors can be equal is if the oriented angle between them is zero (i.e., they point in the same direction). The orientation of the space and the vectors in the space are given as parameters.
More concisely: In a 2-dimensional real inner product space, if the oriented angle between two non-zero vectors is non-zero, then the vectors are not equal.
|
Orientation.oangle_sign_smul_add_smul_left
theorem Orientation.oangle_sign_smul_add_smul_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) (r₁ r₂ : ℝ),
(o.oangle (r₁ • x + r₂ • y) y).sign = SignType.sign r₁ * (o.oangle x y).sign
The theorem `Orientation.oangle_sign_smul_add_smul_left` states that for a two-dimensional real inner product space `V`, given an orientation `o` of `V`, two vectors `x` and `y` in `V`, and two real numbers `r₁` and `r₂`, the sign of the angle between the vector resulting from the linear combination `r₁ • x + r₂ • y` and the vector `y` (denoted `(o.oangle (r₁ • x + r₂ • y) y).sign`) is equal to the product of the sign of `r₁` (`SignType.sign r₁`) and the sign of the angle between `x` and `y` (`(o.oangle x y).sign`).
In simpler terms, this theorem describes how the sign of the angle between a linear combination of two vectors and one of the vectors is influenced by the sign of the scalar multiple of the first vector in the combination and the sign of the angle between the original two vectors.
More concisely: The sign of the angle between a vector and a linear combination of two other vectors is equal to the product of the sign of the scalar multiples and the sign of the angle between the two original vectors.
|
Orientation.oangle_map_complex
theorem Orientation.oangle_map_complex :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (f : V ≃ₗᵢ[ℝ] ℂ),
(Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation →
∀ (x y : V), o.oangle x y = ↑((starRingEnd ℂ) (f x) * f y).arg
The theorem `Orientation.oangle_map_complex` states that for an oriented real inner product space of dimension 2, the oriented angle can be calculated using a complex-number representation of the space. Specifically, given an orientation `o` of the space and a bounded linear isomorphism `f` from the space to the complex numbers such that the mapping of the orientation by `f` equals the standard orientation on the complex numbers, the oriented angle between any two vectors `x` and `y` in the space is equal to the argument of the complex number obtained by conjugating `f(x)` and multiplying by `f(y)`.
More concisely: For an oriented 2-dimensional real inner product space and a bounded linear isomorphism preserving orientation to the complex numbers, the oriented angle between two vectors is equal to the argument of the product of their complex representations, conjugated.
|
Orientation.right_ne_zero_of_oangle_sign_eq_one
theorem Orientation.right_ne_zero_of_oangle_sign_eq_one :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
(o.oangle x y).sign = 1 → y ≠ 0
This theorem states that if the orientation angle between two vectors in a 2-dimensional real inner product space has a positive sign, then the second vector must be non-zero. Here, 'Orientation' is a type representing the orientation of a module (which could be thought of as a generalization of vectors), and 'oangle' is a function that computes the orientation angle between two vectors. The condition `FiniteDimensional.finrank ℝ V = 2` ensures that the vector space is two-dimensional. The sign function applied to the orientation angle, `(o.oangle x y).sign`, returns either -1, 0 or 1, indicating the orientation of the angle (negative, zero or positive respectively). The theorem then asserts that if this sign is 1 (i.e., the angle orientation is positive), then the second vector `y` cannot be the zero vector.
More concisely: If the orientation angle between two vectors in a 2-dimensional real inner product space has a positive sign, then one of the vectors is non-zero.
|
Orientation.oangle_sub_right
theorem Orientation.oangle_sub_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y z : V},
x ≠ 0 → y ≠ 0 → z ≠ 0 → o.oangle x z - o.oangle y z = o.oangle x y
The theorem `Orientation.oangle_sub_right` states that for any three non-zero vectors `x`, `y`, and `z` in a 2-dimensional inner product space `V` over the real numbers, equipped with a given orientation `o`, the difference between the angles made by `x` and `z`, and `y` and `z`, is equal to the angle between `x` and `y`. This theorem is a geometric property that holds in 2-dimensional space.
More concisely: In a 2-dimensional real inner product space with given orientation, the difference between the angles between vectors `x`, `z`, and between `y`, `z` is equal to the angle between `x` and `y`.
|
Orientation.right_ne_zero_of_oangle_ne_zero
theorem Orientation.right_ne_zero_of_oangle_ne_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y ≠ 0 → y ≠ 0
The theorem `Orientation.right_ne_zero_of_oangle_ne_zero` is stating that for any two vectors `x` and `y` in a real inner product space `V` of finite dimension 2, if the oriented angle `oangle` from `x` to `y`, modulo `2 * π`, is nonzero, then the second vector `y` is nonzero. In other words, if the oriented angle between two vectors is distinct from zero, then the second vector cannot be the zero vector.
More concisely: If the oriented angle between two non-zero vectors in a 2-dimensional real inner product space is nonzero, then the second vector is also nonzero.
|
Orientation.angle_eq_iff_oangle_eq_of_sign_eq
theorem Orientation.angle_eq_iff_oangle_eq_of_sign_eq :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {w x y z : V},
w ≠ 0 →
x ≠ 0 →
y ≠ 0 →
z ≠ 0 →
(o.oangle w x).sign = (o.oangle y z).sign →
(InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle y z)
This theorem states that for a real inner product space `V` of finite dimension 2, given an orientation `o` and four non-zero vectors `w`, `x`, `y`, and `z`, if the signs of the two oriented angles between `w` & `x` and `y` & `z` are equal, then the unoriented angles between `w` & `x` and `y` & `z` are equal if and only if the corresponding oriented angles are equal.
In simpler terms, it says that in a 2-dimensional space, if two pairs of vectors create oriented angles with the same sign (either both positive or both negative), then the unoriented angles (i.e., the absolute values of the angles ignoring their direction) between the pairs of vectors are equal if and only if the oriented angles themselves (i.e., angles with their direction of rotation taken into account) are equal.
More concisely: In a 2-dimensional real inner product space, the unoriented angles between two pairs of vectors are equal if and only if their corresponding oriented angles have the same sign.
|
Orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero
theorem Orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
x = 0 ∨ y = 0 ∨ o.oangle x y = ↑(Real.pi / 2) ∨ o.oangle x y = ↑(-Real.pi / 2) ↔ ⟪x, y⟫_ℝ = 0
This theorem states that for a real inner product space of finite rank 2 with a given orientation, one or both of two vectors are zero, or the oriented angle between them is either plus or minus π/2, if and only if their inner product is zero. In other words, it establishes a direct correspondence between the inner product of two vectors being zero and either one or both of the vectors being zero or the angle between them being orthogonal, in the context of a 2-dimensional real inner product space.
More concisely: In a 2-dimensional real inner product space with fixed orientation, two non-zero vectors are orthogonal if and only if their inner product is zero.
|
Orientation.oangle_sign_sub_smul_right
theorem Orientation.oangle_sign_sub_smul_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) (r : ℝ),
(o.oangle x (y - r • x)).sign = (o.oangle x y).sign
This theorem states that for a real inner product space `V` of dimension 2 with a specified orientation `o`, and given vectors `x` and `y` in `V` along with a real number `r`, the sign of the oriented angle `o.oangle` from `x` to `y - r • x` (where `r • x` is the scalar multiplication of `x` by `r`) is the same as the sign of the oriented angle from `x` to `y`. In other words, subtracting a multiple of the first vector from the second vector does not affect the sign of the oriented angle between them.
More concisely: For any real inner product space of dimension 2 with orientation `o`, the sign of the oriented angle from `x` to `y` is equal to the sign of the oriented angle from `x` to `(y - r • x)`, where `r` is a real number.
|
Orientation.two_zsmul_oangle_smul_right_self
theorem Orientation.two_zsmul_oangle_smul_right_self :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) {r : ℝ},
2 • o.oangle x (r • x) = 0
The theorem `Orientation.two_zsmul_oangle_smul_right_self` states that, for a vector space `V` that is a Normed Additive Commutative Group and an Inner Product Space over the Real numbers `ℝ` with a finite rank of 2, and for any orientation `o` of `V` and any vector `x` in `V` and real number `r`, twice the angle (`o.oangle`) between vector `x` and the vector obtained by scaling `x` with `r` (i.e., `r • x`) is always zero. This implies that the angle between a vector and its multiple is always zero degrees.
More concisely: For any 2-dimensional Normed Additive Commutative Group and Inner Product Space over the Real numbers with orientation `o`, the angle between a vector `x` and its multiple `r • x` is always zero.
|
Orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero
theorem Orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
(o.oangle x y).sign = 0 →
x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = Real.pi
The theorem states that if the sign of the oriented angle between two vectors in a real two-dimensional inner product space is zero, then either one of the vectors is the zero vector, or the undirected angle between them is 0 (meaning the vectors are in the same direction) or $\pi$ (meaning the vectors are in opposite directions).
More concisely: In a real two-dimensional inner product space, if the orientation angle between two vectors is zero, then they are either identical or antiparallel.
|
Orientation.oangle_sign_sub_right_eq_neg
theorem Orientation.oangle_sign_sub_right_eq_neg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
(o.oangle x (x - y)).sign = -(o.oangle x y).sign
This theorem states that for a given orientation `o` of a real inner product space `V` of finite rank 2, and any two vectors `x` and `y` in `V`, the sign of the angle `o.oangle` of `x` and `x - y` is the negative of the sign of the angle `o.oangle` of `x` and `y`. In other words, subtracting the second vector `y` from the first vector `x` when computing the angle flips the sign of the angle.
More concisely: For any orientation `o` of a finite-rank 2 real inner product space `V` and vectors `x, y` in `V`, the signed angle between `x` and `x - y` is the negative of the signed angle between `x` and `y`.
|
Orientation.eq_iff_norm_eq_and_oangle_eq_zero
theorem Orientation.eq_iff_norm_eq_and_oangle_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
x = y ↔ ‖x‖ = ‖y‖ ∧ o.oangle x y = 0
The theorem `Orientation.eq_iff_norm_eq_and_oangle_eq_zero` states that for any two vectors `x` and `y` in a 2-dimensional normed additively commutative group `V` with an inner product space over the real numbers and a given orientation `o`, these vectors are equal if and only if the norm of `x` equals the norm of `y` and the orientation-angle between `x` and `y` is zero. In other words, two vectors in a 2-dimensional real vector space are identical precisely when they have the same length and there is no angle between them according to a specified orientation.
More concisely: In a 2-dimensional real inner product space with a given orientation, two vectors have the same direction and length if and only if they are equal.
|
Orientation.left_ne_zero_of_oangle_eq_pi_div_two
theorem Orientation.left_ne_zero_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → x ≠ 0
The theorem `Orientation.left_ne_zero_of_oangle_eq_pi_div_two` asserts that in a real inner product space `V` of finite dimension equal to 2, for any orientation `o` and two vectors `x` and `y`, if the oriented angle from `x` to `y` is `π / 2`, then the vector `x` must be nonzero. This essentially captures the geometric intuition that if two vectors are orthogonal (i.e., the angle between them is 90 degrees), then neither of them can be the zero vector.
More concisely: In a 2-dimensional real inner product space, if the oriented angle between non-zero vectors `x` and `y` is equal to `π/2`, then their difference `x - y` is a non-zero vector.
|
Orientation.oangle_eq_angle_or_eq_neg_angle
theorem Orientation.oangle_eq_angle_or_eq_neg_angle :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
x ≠ 0 →
y ≠ 0 → o.oangle x y = ↑(InnerProductGeometry.angle x y) ∨ o.oangle x y = -↑(InnerProductGeometry.angle x y)
This theorem states that in a 2-dimensional real vector space, the oriented angle between two nonzero vectors is either equal to or the negative of the unoriented angle between those two vectors. Here, the oriented angle is a measure of the angle from one vector to the other, taking into account the direction of rotation (and defined to be 0 if either vector is 0), while the unoriented angle is the measure of the smallest angle between two vectors, without consideration for the direction of rotation (and defined to be π/2 if either vector is 0).
More concisely: In a 2-dimensional real vector space, the oriented angle between two nonzero vectors is equal to the unoriented angle with its sign determined by their cross product's sign.
|
Orientation.oangle_sign_neg_right
theorem Orientation.oangle_sign_neg_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
(o.oangle x (-y)).sign = -(o.oangle x y).sign
This theorem, `Orientation.oangle_sign_neg_right`, states that for any normed additive commutative group `V` equipped with a real inner product space and an orientation `o`, if the vector space `V` has a finite rank equal to 2, then negating the second vector passed to the function `oangle` results in negation of the sign of the angle. In other words, the sign of the angle between two vectors `x` and `y` in `V` is negative when the vector `y` is negated.
More concisely: For any 2-dimensional normed additive commutative group `V` equipped with a real inner product space and orientation `o`, the sign of `oangle(x, y)` is negative when `y` is negated.
|
Orientation.right_ne_zero_of_oangle_eq_pi_div_two
theorem Orientation.right_ne_zero_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → y ≠ 0
The theorem `Orientation.right_ne_zero_of_oangle_eq_pi_div_two` states that in a real 2-dimensional inner product space, if the oriented angle from a vector `x` to another vector `y` is equal to `π / 2` radians, then the second vector `y` cannot be the zero vector. The orientation of the space is given by `o`, and the theorem assures that if `y` forms a right angle (i.e., a `90°` or `π/2` radian angle) with `x`, then `y` must be non-zero.
More concisely: In a real 2-dimensional inner product space, if the oriented angle between non-zero vectors x and y is equal to π/2, then y is neither a scalar multiple nor the zero vector of x.
|
Orientation.oangle_eq_of_angle_eq_of_sign_eq
theorem Orientation.oangle_eq_of_angle_eq_of_sign_eq :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {w x y z : V},
InnerProductGeometry.angle w x = InnerProductGeometry.angle y z →
(o.oangle w x).sign = (o.oangle y z).sign → o.oangle w x = o.oangle y z
In the context of an inner product space over the real numbers, with a normed additively commutative group structure, and finite dimensional with rank 2, this theorem states that if two unoriented angles (between vectors `w` and `x`, and `y` and `z` respectively) are equal, and the signs of the corresponding oriented angles (oriented by a given orientation `o`) are also equal, then the oriented angles themselves are equal. This is true even in degenerate cases where the vectors may not form a standard geometric angle.
More concisely: In a finite-dimensional, inner product space over the real numbers with rank 2, if the unoriented angles between two pairs of vectors and their corresponding oriented angles (w.r.t. a given orientation) are equal, then the oriented angles are equal.
|
Orientation.right_ne_zero_of_oangle_sign_eq_neg_one
theorem Orientation.right_ne_zero_of_oangle_sign_eq_neg_one :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
(o.oangle x y).sign = -1 → y ≠ 0
The theorem `Orientation.right_ne_zero_of_oangle_sign_eq_neg_one` states that given a normed additive commutative group `V`, which also forms an inner product space over the real numbers `ℝ`, and given that `V` has a finite rank of 2, then for any orientation `o` of `V` and any two vectors `x` and `y` in `V`, if the sign of the angle between `x` and `y` (according to the orientation `o`) is `-1`, then the second vector `y` cannot be the zero vector. In simpler terms, if the orientation-based angle between two vectors is negative, the second vector is non-zero.
More concisely: Given a 2-dimensional inner product space over the real numbers with finite basis, if the angle between two vectors according to a fixed orientation is negative, then those vectors are linearly independent and neither is the zero vector.
|
Orientation.oangle_smul_right_of_neg
theorem Orientation.oangle_smul_right_of_neg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) {r : ℝ},
r < 0 → o.oangle x (r • y) = o.oangle x (-y)
This theorem states that in a real, two-dimensional, inner product space with a given orientation, the angle between vectors x and ry (where r is a negative real number) is the same as the angle between vectors x and -y. Specifically, `Orientation.oangle_smul_right_of_neg` states that for all normed add commutative groups `V` with an inner product space structure over the real numbers, if the finite rank of `V` over the real numbers is equal to 2, then for any orientation `o` of `V` and any vectors `x` and `y` in `V`, and for any real number `r` less than zero, the angle `o.oangle` between `x` and `ry` is equal to the angle `o.oangle` between `x` and `-y`.
More concisely: In a real, two-dimensional inner product space with a given orientation, the angle between vector x and -ry (where r is a negative real number) equals the angle between vector x and -y.
|
Orientation.oangle_add_cyc3
theorem Orientation.oangle_add_cyc3 :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y z : V},
x ≠ 0 → y ≠ 0 → z ≠ 0 → o.oangle x y + o.oangle y z + o.oangle z x = 0
The theorem `Orientation.oangle_add_cyc3` states that given a real inner product space `V` of finite rank 2 and an orientation `o` of this space, for any three nonzero vectors `x`, `y`, and `z` from `V`, the sum of the oriented angles between `x` and `y`, `y` and `z`, and `z` and `x` (in cyclic order), equals zero. This theorem is essentially a formalization of the geometric fact about the sum of the angles in a triangle.
More concisely: Given a real inner product space of finite rank 2 with orientation, the sum of the oriented angles between any three nonzero vectors is zero in cyclic order.
|
Orientation.left_ne_zero_of_oangle_sign_eq_neg_one
theorem Orientation.left_ne_zero_of_oangle_sign_eq_neg_one :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
(o.oangle x y).sign = -1 → x ≠ 0
This theorem states that given a two-dimensional real inner product space `V`, and an orientation `o` of this space, if the sign of the oriented angle between two vectors `x` and `y` (according to orientation `o`) is `-1`, then the first vector `x` cannot be the zero vector. Hence, a negative sign of the oriented angle implies the non-zero nature of the first vector in the context of a 2D real inner product space.
More concisely: In a 2D real inner product space and for an orientation, if the oriented angle between two vectors has a negative sign, then the first vector is non-zero.
|
Orientation.oangle_neg_self_left
theorem Orientation.oangle_neg_self_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V},
x ≠ 0 → o.oangle (-x) x = ↑Real.pi
This theorem states that in a 2-dimensional real inner product space V, the angle between a nonzero vector `x` and its negation `-x` is `π` radians. The orientation of the space is denoted by `o`. For every nonzero vector `x`, when measured in the orientation `o`, the angle between `x` and `-x` is `π` radians, which is equivalent to a straight angle or 180 degrees. This result is intuitive as the negation of a vector points in the exact opposite direction of the original vector.
More concisely: In a 2-dimensional real inner product space, the angle between a nonzero vector and its negation is π radians (180 degrees).
|
Orientation.left_ne_zero_of_oangle_eq_neg_pi_div_two
theorem Orientation.left_ne_zero_of_oangle_eq_neg_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(-Real.pi / 2) → x ≠ 0
This theorem states that if we have a vector space `V` over real numbers that is equipped with an inner product and a norm, and this vector space is two-dimensional, then for any orientation `o` and any two vectors `x` and `y` in `V`, if the angle between `x` and `y` according to `o` is `-π / 2`, then the vector `x` is not the zero vector. This means that in a two-dimensional real inner product space, if two vectors are oriented such that they make an angle of `-π / 2` radians (or 90 degrees clockwise), then the first vector cannot be a zero vector.
More concisely: In a two-dimensional real inner product space, if the angle between two non-zero vectors is -π/2, then they are orthogonal (i.e., their inner product is zero) but neither is the zero vector.
|
Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two
theorem Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → ⟪y, x⟫_ℝ = 0
This theorem states that in a real inner product space with finite dimension of 2, if the oriented angle between two vectors is equal to π/2 (or equivalently 90 degrees), then the inner product of the reversed order of these vectors is zero. This essentially corresponds to the geometric idea that if two vectors are orthogonal, i.e., they form a 90 degree angle, their inner (or dot) product is zero.
More concisely: In a 2-dimensional real inner product space, the inner product of two orthogonal vectors is zero.
|
Orientation.oangle_smul_add_right_eq_zero_or_eq_pi_iff
theorem Orientation.oangle_smul_add_right_eq_zero_or_eq_pi_iff :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (r : ℝ),
o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = ↑Real.pi ↔ o.oangle x y = 0 ∨ o.oangle x y = ↑Real.pi
This theorem is a technical lemma used in the proof of another theorem, namely `oangle_sign_smul_add_right`, and is not designed to be used in isolation. It states that for a real inner product space `V` of finite dimension 2, given an orientation `o` and vectors `x` and `y` in `V`, as well as a real number `r`, the oriented angle `o.oangle` from `x` to `r • x + y` (where `r • x` denotes the scalar multiplication of `r` and `x`) is either 0 or π if and only if the oriented angle from `x` to `y` is either 0 or π. Note that this statement involves some concepts from linear algebra such as the orientation of a vector space and the notion of an oriented angle. The symbol `↑Real.pi` represents the real number π, the ratio of a circle's circumference to its diameter.
More concisely: For a real inner product space of dimension 2 with orientation and vectors `x`, `y`, and scalar `r`, the oriented angles from `x` to `r • x + y` and from `x` to `y` are either both 0 or both π.
|
Orientation.two_zsmul_oangle_neg_right
theorem Orientation.two_zsmul_oangle_neg_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
2 • o.oangle x (-y) = 2 • o.oangle x y
This theorem states that for a 2-dimensional real inner product space `V` with any given orientation `o`, and for any two vectors `x` and `y` in `V`, twice the oriented angle `o.oangle` from `x` to `-y` (the negation of `y`) is equal to twice the oriented angle from `x` to `y`. In simple terms, negating the second vector does not change twice the angle between the vectors in the given orientation of the vector space.
More concisely: For any 2-dimensional real inner product space `V` with orientation `o`, and vectors `x` and `y` in `V`, the angle `o.oangle` from `x` to `-y` equals the angle from `x` to `y`.
|
Orientation.oangle_sign_smul_add_right
theorem Orientation.oangle_sign_smul_add_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) (r : ℝ),
(o.oangle x (r • x + y)).sign = (o.oangle x y).sign
The theorem `Orientation.oangle_sign_smul_add_right` states that for any real number `r` and vectors `x` and `y` in a real 2-dimensional inner product space `V` with an orientation `o`, the sign of the oriented angle from `x` to `r • x + y` (i.e., the vector obtained by scaling `x` by `r` and adding `y`) is the same as the sign of the oriented angle from `x` to `y`. Here, the "sign" of an angle is defined as `0` if the angle is `0` or `π`, `1` if the angle is strictly between `0` and `π`, and `-1` if the angle is strictly between `-π` and `0`. This property essentially says that adding a scalar multiple of one vector to another doesn't change the overall direction of the angle between them.
More concisely: The sign of the oriented angle between vectors `x` and `r * x + y` in a 2-dimensional inner product space with orientation `o` is equal to the sign of the oriented angle between `x` and `y`.
|
Orientation.two_zsmul_oangle_smul_smul_self
theorem Orientation.two_zsmul_oangle_smul_smul_self :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) {r₁ r₂ : ℝ},
2 • o.oangle (r₁ • x) (r₂ • x) = 0
This theorem, named `Orientation.two_zsmul_oangle_smul_smul_self`, states that for a real inner product space `V` with a finite dimension of 2 and a given orientation `o`, the double of the angle between two scalar multiples (by `r₁` and `r₂` respectively) of a vector `x` in `V` is always 0. In other words, the angle between any two multiples of the same vector in a two-dimensional real inner product space is invariant and does not depend on the multiples used.
More concisely: In a two-dimensional real inner product space with a fixed orientation, the angle between two scalar multiples of the same vector is always equal.
|
Orientation.oangle_eq_neg_angle_of_sign_eq_neg_one
theorem Orientation.oangle_eq_neg_angle_of_sign_eq_neg_one :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
(o.oangle x y).sign = -1 → o.oangle x y = -↑(InnerProductGeometry.angle x y)
This theorem states that the oriented angle between two vectors equals the negative of the unoriented angle if the sign of the oriented angle is negative. This theorem holds in a real inner product space with a finite dimension of 2. This means that in a 2D space, if the orientation of the angle between two vectors 'x' and 'y' is clockwise (negative), then the magnitude of the oriented angle is equal to the negative of the magnitude of the unoriented angle. The unoriented angle is simply the angle between the two vectors without considering any orientation.
More concisely: In a 2D real inner product space, the magnitude of the negatively oriented angle between vectors x and y is equal to the negative of the magnitude of the unoriented angle.
|
Orientation.oangle_smul_right_self_of_nonneg
theorem Orientation.oangle_smul_right_self_of_nonneg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) {r : ℝ},
0 ≤ r → o.oangle x (r • x) = 0
This theorem states that the angle between a vector and a nonnegative multiple of that vector is zero. Specifically, for any normed additive commutative group `V` which is also an inner product space over the field of real numbers ℝ with finite dimension equal to 2, any orientation `o` of `V`, any vector `x` in `V`, and any nonnegative real number `r`, the oriented angle `o.oangle` between the vector `x` and the vector obtained by scaling `x` by `r` (`r • x`) is zero. This makes intuitive sense as scaling a vector does not change its direction, hence, the angle remains zero.
More concisely: For any 2-dimensional inner product space V over ℝ, oriented angle(x, r • x) = 0 for all vectors x in V and nonnegative scalars r.
|
Orientation.oangle_smul_smul_self_of_nonneg
theorem Orientation.oangle_smul_smul_self_of_nonneg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) {r₁ r₂ : ℝ},
0 ≤ r₁ → 0 ≤ r₂ → o.oangle (r₁ • x) (r₂ • x) = 0
This theorem states that in a real inner product space `V` of dimension 2, if we have two nonnegative scalars `r₁` and `r₂` and a vector `x` in `V`, then the angle between the vectors resulting from scaling `x` by `r₁` and `r₂` (represented by `r₁ • x` and `r₂ • x` respectively) is 0. This means that in the given orientation `o` of the vector space, these two vectors are in the same direction.
More concisely: In a real inner product space of dimension 2, the angles between vectors `r₁ • x` and `r₂ • x` are zero, implying they are in the same direction for any nonnegative scalars `r₁` and `r₂` and vector `x`.
|
Orientation.oangle_eq_zero_iff_sameRay
theorem Orientation.oangle_eq_zero_iff_sameRay :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = 0 ↔ SameRay ℝ x y
The theorem `Orientation.oangle_eq_zero_iff_sameRay` states that for a 2-dimensional real inner product vector space `V` with a given orientation `o`, the oriented angle between any two vectors `x` and `y` in this space is zero if and only if these vectors are on the same ray. In this context, vectors are considered to be on the same ray if one is zero or if there exist positive scalars such that one vector is a positive multiple of the other.
More concisely: For any orientation `o` on a 2-dimensional real inner product vector space `V` and vectors `x` and `y` in `V`, the oriented angle between `x` and `y` is zero if and only if `x` and `y` are on the same ray.
|
Orientation.two_zsmul_oangle_smul_right_of_ne_zero
theorem Orientation.two_zsmul_oangle_smul_right_of_ne_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) {r : ℝ},
r ≠ 0 → 2 • o.oangle x (r • y) = 2 • o.oangle x y
This theorem states that for a two-dimensional real inner product space, given an orientation of this space, two vectors `x` and `y`, and a nonzero real number `r`, the statement `2 • o.oangle x (r • y) = 2 • o.oangle x y` holds true. In other words, if you multiply the second vector `y` by a nonzero real number `r`, then the twice the angle between vectors `x` and `r • y` (the scaled vector) is unchanged and equals to twice the angle between vectors `x` and `y`. This emphasizes that scaling the second vector does not affect the overall orientation or twice the angle between the two vectors.
More concisely: For any orientation `o`, vectors `x` and `y` in a 2-dimensional real inner product space, and nonzero real number `r`, the twice the angle between `x` and `r•y` is equal to twice the angle between `x` and `y`.
|
Orientation.oangle_eq_angle_of_sign_eq_one
theorem Orientation.oangle_eq_angle_of_sign_eq_one :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
(o.oangle x y).sign = 1 → o.oangle x y = ↑(InnerProductGeometry.angle x y)
The theorem `Orientation.oangle_eq_angle_of_sign_eq_one` states that, given a normed additive commutative group `V` equipped with an inner product space over real numbers (ℝ) which is two-dimensional, an orientation `o` of `V`, and any two vectors `x` and `y` in `V`, if the sign of the oriented angle between `x` and `y` is positive (i.e., `1`), then the oriented angle between `x` and `y` is equal to the unoriented angle between `x` and `y`. This theorem formalizes the intuitive notion that a positive oriented angle in a two-dimensional space corresponds to the standard "counterclockwise" angle measurement.
More concisely: If the oriented angle between two vectors in a 2-dimensional inner product space is positive, then it equals the unoriented angle between them.
|
Orientation.oangle_add_oangle_rev_neg_right
theorem Orientation.oangle_add_oangle_rev_neg_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
o.oangle x (-y) + o.oangle y (-x) = 0
The theorem `Orientation.oangle_add_oangle_rev_neg_right` states that for any normed additively commutative group `V` that is also an inner product space over the real numbers `ℝ`, with a finite dimensionality of 2, and for any given orientation `o` of this space, the sum of the oriented angles between any two vectors `x` and `y` in `V`, where the second vector in each pair is negated, is always zero. In other words, it states that in a 2-dimensional real inner product space, the orientation-specific angle between a vector `x` and the negation of a vector `y`, added to the orientation-specific angle between `y` and the negation of `x`, equals zero.
More concisely: In a 2-dimensional real inner product space, the sum of the oriented angles between a vector and its negated counterpart, taken over all pairs of vectors, is zero for any given orientation.
|
Orientation.oangle_sign_add_left
theorem Orientation.oangle_sign_add_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
(o.oangle (x + y) y).sign = (o.oangle x y).sign
This is a theorem about the orientation of a 2-dimensional real inner product space. It states that for any given orientation `o` of the space, and any two vectors `x` and `y` in that space, the sign of the angle between the sum of `x` and `y` and `y` itself is the same as the sign of the angle between `x` and `y`. In other words, adding the second vector `y` to the first vector `x` does not change the sign of the angle between them according to the specified orientation `o`.
More concisely: For any orientation of a 2-dimensional real inner product space and vectors `x` and `y` in that space, the sign of the angle between `x + y` and `y` equals the sign of the angle between `x` and `y`.
|
Orientation.inner_eq_zero_of_oangle_eq_pi_div_two
theorem Orientation.inner_eq_zero_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → ⟪x, y⟫_ℝ = 0
This theorem states that if the oriented angle between two vectors in a real 2-dimensional inner product space is π/2, then the inner product of these vectors is zero. In other words, if two vectors are oriented at a right angle to each other, their inner product (or dot product) is zero, which is a fundamental characteristic of orthogonal vectors in Euclidean space. The orientation of the space and the two vectors are taken as inputs for this theorem.
More concisely: In a real 2-dimensional inner product space, the inner product of two vectors with an oriented angle of π/2 (a right angle) is zero.
|
Orientation.continuousAt_oangle
theorem Orientation.continuousAt_oangle :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V × V},
x.1 ≠ 0 → x.2 ≠ 0 → ContinuousAt (fun y => o.oangle y.1 y.2) x
The theorem `Orientation.continuousAt_oangle` states that, in a two-dimensional real inner product space, the oriented angle function, which takes a pair of vectors and returns an angle with a specific orientation, is continuous at a pair of non-zero vectors. This essentially means that as the input vectors get arbitrarily close to the given pair, the output angle also gets arbitrarily close to the angle of the initial pair. This continuity holds true only when the vectors involved are non-zero.
More concisely: In a 2-dimensional real inner product space, the oriented angle function between two non-zero vectors is a continuous function.
|
Orientation.two_zsmul_oangle_neg_left
theorem Orientation.two_zsmul_oangle_neg_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
2 • o.oangle (-x) y = 2 • o.oangle x y
The theorem `Orientation.two_zsmul_oangle_neg_left` states that for a real inner product space `V` of finite dimension 2, for any orientation `o` and any two vectors `x` and `y` in `V`, doubling the angle determined by the negation of `x` and `y` (`2 • o.oangle (-x) y`) equals to doubling the angle determined by `x` and `y` (`2 • o.oangle x y`). In other words, negating the first vector does not change twice the angle between the two vectors under the given orientation.
More concisely: For any orientation `o` and vectors `x` and `y` in a 2-dimensional real inner product space, `2 * o.oangle (-x) y = 2 * o.oangle x y`.
|
Orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul
theorem Orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = 0 ∨ o.oangle x y = ↑Real.pi ↔ x = 0 ∨ ∃ r, y = r • x
This theorem, named `Orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul`, states that in a real `2`-dimensional inner product space `V`, for any given orientation `o` and any two vectors `x` and `y` in `V`, the oriented angle between `x` and `y` is either `0` or `π` if and only if the vector `x` is the zero vector or the vector `y` is a scalar multiple of `x`. Here, the scalar value is represented by `r` and the operation of multiplying a vector by a scalar is represented by `r • x`.
More concisely: In a real 2-dimensional inner product space, the oriented angle between two vectors is 0 or π if and only if one vector is a scalar multiple of the other.
|
Orientation.left_ne_zero_of_oangle_eq_pi
theorem Orientation.left_ne_zero_of_oangle_eq_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑Real.pi → x ≠ 0
This theorem states that if the angle between two vectors in a 2-dimensional real inner product space is π (which is the lean language representation of the mathematical constant Pi), then the first vector cannot be zero. Here, the space is considered 2-dimensional explicitly by the fact that the rank of the space over the reals is 2. Also, this theorem is considering an orientation of the space. An orientation can be thought of as a choice of which "direction" is "positive".
More concisely: In a 2-dimensional real inner product space with a fixed orientation, the inner product of two non-zero vectors is non-zero if and only if the angle between them is less than π. Therefore, if the angle between two vectors is π, then at least one of the vectors must be the zero vector.
|
Orientation.abs_oangle_sub_left_toReal_lt_pi_div_two
theorem Orientation.abs_oangle_sub_left_toReal_lt_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
‖x‖ = ‖y‖ → |(o.oangle (y - x) y).toReal| < Real.pi / 2
This theorem states that for any isosceles triangle in a real 2-dimensional inner product space, the absolute value of the angle between any base vector and the vector pointing from one base vertex to the other, expressed as an oriented angle, is less than π/2. In other words, a base angle of an isosceles triangle is acute. The condition `‖x‖ = ‖y‖` enforces the isosceles property, that is, the two sides of the triangle adjacent to the base angle have the same length.
More concisely: In a real 2-dimensional inner product space, the base angle of an isosceles triangle is acute, i.e., its absolute value is less than π/2.
|
Orientation.ne_of_oangle_eq_pi
theorem Orientation.ne_of_oangle_eq_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑Real.pi → x ≠ y
The theorem `Orientation.ne_of_oangle_eq_pi` states that for any pair of vectors `x` and `y` in a two-dimensional real inner product space `V` with a given orientation `o`, if the angle between `x` and `y` according to this orientation is equal to `π` (pi), then `x` and `y` cannot be equal. In simpler terms, if two vectors point in exactly opposite directions (making an angle of pi radians), then they cannot be the same vector.
More concisely: In a 2-dimensional real inner product space with given orientation, two non-zero vectors making an angle of pi radians are linearly independent. (Note: this is an equivalent statement to the original theorem, stating that if the angle between two vectors is pi, then they cannot be equal.)
|
Orientation.two_zsmul_oangle_smul_left_self
theorem Orientation.two_zsmul_oangle_smul_left_self :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) {r : ℝ},
2 • o.oangle (r • x) x = 0
This theorem states that for any real-numbered vector `x` in a 2-dimensional real inner product space `V` with a given orientation `o`, and any real number `r`, the orientation of the angle between `r • x` (the vector `x` scaled by `r`) and the vector `x` itself, multiplied by 2, is always 0. This implies that the angle between a vector and its scaled version, in a 2-dimensional space following the specified orientation, is such that its doubled orientation always results in zero.
More concisely: For any vector `x` in a 2-dimensional real inner product space `V` and real number `r`, the angle between `x` and `r • x` has doubled orientation 0.
|
Orientation.oangle_neg_left
theorem Orientation.oangle_neg_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
x ≠ 0 → y ≠ 0 → o.oangle (-x) y = o.oangle x y + ↑Real.pi
This theorem, named `Orientation.oangle_neg_left`, states that for a 2-dimensional real inner product space `V` with an orientation `o` and any two non-zero vectors `x` and `y` from `V`, the orientation angle between the negation of the vector `x` and `y` is the same as the orientation angle between `x` and `y` plus the constant `π`. In other words, negating the first vector that is passed to the `oangle` function adds `π` to the orientation angle.
More concisely: For any 2-dimensional real inner product space `V` with orientation `o`, and vectors `x` and `y` in `V` with `x ≠ 0`, the orientation angle between `-x` and `y` is equal to the angle between `x` and `y` plus `π`.
|
Orientation.angle_eq_abs_oangle_toReal
theorem Orientation.angle_eq_abs_oangle_toReal :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
x ≠ 0 → y ≠ 0 → InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
The theorem `Orientation.angle_eq_abs_oangle_toReal` states that, in a two-dimensional real inner product space (a space with a structure that allows dot products), the unoriented angle between two nonzero vectors is equal to the absolute value of the oriented angle between those vectors when transformed into a real number. An unoriented angle does not consider the direction of rotation, whereas the oriented angle does. The oriented angle is initially represented as a `Real.Angle`, a type that represents angles in radians and supports operations like addition and subtraction modulo $2\pi$, but then it is converted to a real number.
More concisely: The theorem asserts that the absolute value of the oriented angle between two nonzero vectors in a real inner product space equals the unoriented angle between them when expressed as real numbers.
|
Orientation.oangle_sign_smul_right
theorem Orientation.oangle_sign_smul_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) (r : ℝ),
(o.oangle x (r • y)).sign = SignType.sign r * (o.oangle x y).sign
The theorem `Orientation.oangle_sign_smul_right` states that for any real number `r` and any two vectors `x` and `y` in a real inner product space `V` of finite rank 2, scaling the second vector `y` by `r` in the `oangle` function multiplies the sign of the resulting angle by the sign of `r`. This is done with respect to a given orientation `o` of the space `V`. In mathematical terms, if we denote the orientation angle between vectors `x` and `y` in the orientation `o` as `o.oangle x y`, then the theorem asserts that the sign of `o.oangle x (r • y)` is equal to the sign of `r` multiplied by the sign of `o.oangle x y`.
More concisely: For any orientation `o` in a real inner product space of finite rank 2, and real numbers `r` and signs `s_x` and `s_y` such that `x` and `y` are nonzero vectors with `s_x * o.oangle x y` defined, we have `s_x * s_y * o.oangle x (r * y) = s_x * o.oangle x y * |r|`.
|
Orientation.oangle_eq_zero_iff_angle_eq_zero
theorem Orientation.oangle_eq_zero_iff_angle_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
x ≠ 0 → y ≠ 0 → (o.oangle x y = 0 ↔ InnerProductGeometry.angle x y = 0)
This theorem states that the oriented angle between two nonzero vectors is zero if and only if the unoriented angle between them is also zero. This is valid in the context of a two-dimensional real inner product space. Specifically, for any two vectors x and y in a normed add commutative group V, that also forms an inner product space over real numbers ℝ, and has a finite rank of 2, if neither of these vectors is the zero vector, then the oriented angle between them (measured using a specific orientation o) is zero if and only if their unoriented angle is also zero.
More concisely: In a 2-dimensional real inner product space, the oriented angle between two non-zero vectors is zero if and only if their unoriented angle is zero.
|
Orientation.oangle_sign_neg_left
theorem Orientation.oangle_sign_neg_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
(o.oangle (-x) y).sign = -(o.oangle x y).sign
The theorem `Orientation.oangle_sign_neg_left` states that for a two-dimensional real inner product space `V`, if you have an orientation `o` and two vectors `x` and `y` in `V`, then the sign of the angle between `-x` and `y` according to orientation `o` is the negative of the sign of the angle between `x` and `y` according to the same orientation. In simpler terms, it says that flipping one of the vectors in a pair across the origin reverses the orientation of the angle between them.
More concisely: For an orientation `o` in a 2-dimensional real inner product space `V` and vectors `x` and `y` in `V`, the sign of the angle between `-x` and `y` according to `o` is the negative of the sign of the angle between `x` and `y` according to `o`.
|
Orientation.oangle_sign_add_smul_left
theorem Orientation.oangle_sign_add_smul_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) (r : ℝ),
(o.oangle (x + r • y) y).sign = (o.oangle x y).sign
This theorem states that, in a 2-dimensional real vector space endowed with an orientation, the sign of the angle between two vectors remains the same if a multiple of the second vector is added to the first one. In mathematical terms, for any real number `r` and any two vectors `x` and `y`, the sign of the angle between `x + r * y` and `y` is equal to the sign of the angle between `x` and `y`.
More concisely: For any vectors `x`, `y` in a 2-dimensional real vector space with orientation, and real number `r`, the sign of the angle between `x + r*y` and `y` is equal to the sign of the angle between `x` and `y`.
|
Orientation.two_zsmul_oangle_of_span_eq_of_span_eq
theorem Orientation.two_zsmul_oangle_of_span_eq_of_span_eq :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {w x y z : V},
Submodule.span ℝ {w} = Submodule.span ℝ {x} →
Submodule.span ℝ {y} = Submodule.span ℝ {z} → 2 • o.oangle w y = 2 • o.oangle x z
This theorem states that, given a 2-dimensional real inner product space `V` with a specified orientation `o`, if the span of singleton sets containing vectors `w` and `x` are equal, and the span of singleton sets containing vectors `y` and `z` are also equal, then twice the oriented angle between `w` and `y` is equal to twice the oriented angle between `x` and `z`. In other words, if vectors `w` and `x` lie on the same line through the origin, and vectors `y` and `z` also lie on the same line through the origin, then the angles formed by `w`, `y` and `x`, `z` (respecting the orientation `o`) are the same when multiplied by two.
More concisely: Given a 2-dimensional real inner product space with a specified orientation, if the lines through the origin containing vectors (w, x) and (y, z) are equal, then twice the oriented angle between w and y is equal to twice the oriented angle between x and z.
|
Orientation.oangle_eq_pi_iff_angle_eq_pi
theorem Orientation.oangle_eq_pi_iff_angle_eq_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑Real.pi ↔ InnerProductGeometry.angle x y = Real.pi
This theorem states that, given a real inner product space `V` of finite rank 2, for any orientation `o` of `V` and any vectors `x` and `y` in `V`, the oriented angle between `x` and `y` (measured with respect to `o`) is equal to π if and only if the unoriented angle between `x` and `y` is also π. Here, π is the mathematical constant approximately equal to 3.14159, representing the ratio of the circumference of a circle to its diameter. The "oriented angle" between two vectors considers the direction (from `x` to `y` or vice versa), while the "unoriented angle" only considers the magnitude of the angle, regardless of the direction.
More concisely: Given a real inner product space of finite rank 2, the oriented angle equals the unoriented angle (both in radians) between two vectors if and only if they are orthogonal and have the same magnitude.
|
Orientation.two_zsmul_oangle_neg_self_left
theorem Orientation.two_zsmul_oangle_neg_self_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V),
2 • o.oangle (-x) x = 0
This theorem states that for any real normed additive commutative group `V` that is also an inner product space, and has a finite rank equal to 2 (indicating a two-dimensional space), the angle between a vector `x` and its negation `-x`, when doubled, is equal to 0. This is true for any orientation `o` of the vector space `V`. In mathematical terms, 2 times the angle between `-x` and `x` is 0.
This essentially says that a vector and its negation have the same orientation in a two-dimensional real inner product space.
More concisely: In a two-dimensional real inner product space, the angle between a vector and its negation is 0.
|
Orientation.oangle_add_oangle_rev
theorem Orientation.oangle_add_oangle_rev :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
o.oangle x y + o.oangle y x = 0
This theorem states that, in a 2-dimensional inner product space over real numbers, the sum of the oriented angles of two vectors `x` and `y` taken in both orders (`x` to `y` and `y` to `x`) is zero. The orientation of the space is given by `o`, a function from a finite type `Fin 2` to the space of scalars. In other words, if you calculate the oriented angle from vector `x` to vector `y`, and then calculate the oriented angle from vector `y` back to vector `x`, their sum will always be zero, no matter the vectors and the orientation of the space.
More concisely: In a 2-dimensional real inner product space with orientation function `o`, the sum of the oriented angles between vectors `x` and `y` and `y` and `x` is zero: `angle o x y + angle o y x = 0`.
|
Orientation.oangle_self
theorem Orientation.oangle_self :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V), o.oangle x x = 0
This theorem states that for any two-dimensional real vector space `V` equipped with a normed additive commutative group structure and an inner product space over the real numbers, and for any orientation `o` of `V` and any vector `x` in `V`, the oriented angle from `x` to itself, denoted by `Orientation.oangle o x x`, is always zero. This is a mathematical statement about geometry, which asserts that the angle that a vector forms with itself in a given orientation is always zero.
More concisely: For any two-dimensional real vector space `V` endowed with a normed additive commutative group structure and an inner product space structure over the real numbers, and for any orientation `o` and vector `x` in `V`, the oriented angle `oangle o x x` is equal to zero.
|
Orientation.inner_eq_zero_of_oangle_eq_neg_pi_div_two
theorem Orientation.inner_eq_zero_of_oangle_eq_neg_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(-Real.pi / 2) → ⟪x, y⟫_ℝ = 0
This theorem states that in a real inner product space of dimension 2, if the oriented angle between two vectors is negative half of Pi (-π / 2), then the inner product of these two vectors is zero. In other words, the two vectors are orthogonal to each other. This is valid for any orientation of the space. The oriented angle is calculated with respect to this orientation.
More concisely: In a 2-dimensional real inner product space, two vectors are orthogonal if and only if the oriented angle between them is -π/2.
|
Orientation.cos_oangle_eq_cos_angle
theorem Orientation.cos_oangle_eq_cos_angle :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
x ≠ 0 → y ≠ 0 → (o.oangle x y).cos = (InnerProductGeometry.angle x y).cos
This theorem states that the cosine of the oriented angle between two nonzero vectors is equal to the cosine of the unoriented angle between those vectors. More specifically, given a 2-dimensional real inner product space `V`, an orientation `o` of `V`, and two nonzero vectors `x` and `y` in `V`, the cosine of the oriented angle between `x` and `y` under the orientation `o` is the same as the cosine of the unoriented angle between `x` and `y`. This orientation-sensitive angle is represented with the `o.oangle` function, while the orientation-insensitive angle is represented with the `InnerProductGeometry.angle` function.
More concisely: The cosine of the oriented angle between two nonzero vectors in a 2-dimensional real inner product space, under a given orientation, equals the cosine of the unoriented angle between those vectors.
|
Orientation.oangle_sign_smul_left
theorem Orientation.oangle_sign_smul_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) (r : ℝ),
(o.oangle (r • x) y).sign = SignType.sign r * (o.oangle x y).sign
The theorem `Orientation.oangle_sign_smul_left` states that for any real inner product space `V` of finite dimension 2, for any orientation `o` of this space, for any vectors `x`, `y` in `V` and for any real number `r`, the sign of the angle formed by the vector `r • x` and `y` under the orientation `o` is equal to the product of the sign of `r` and the sign of the angle between `x` and `y` under the same orientation. This implies that scaling the first vector by a real factor changes the sign of the angle by the sign of the real factor.
More concisely: For any orientation of a 2-dimensional real inner product space, the sign of the angle between `r * x` and `y` is equal to the product of the sign of `r` and the sign of the angle between `x` and `y`.
|
Orientation.ne_of_oangle_sign_eq_one
theorem Orientation.ne_of_oangle_sign_eq_one :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
(o.oangle x y).sign = 1 → x ≠ y
This theorem states that if the orientation of two vectors `x` and `y` in a two-dimensional real inner product space `V` (i.e., a space equipped with an operation that mirrors the general concept of dot product in Euclidean space) yields a sign of 1, then the two vectors `x` and `y` cannot be equal. In other words, it asserts that the angle between two equal vectors cannot have a positive orientation, under the assumption that the space `V` over real numbers is two-dimensional.
More concisely: In a two-dimensional real inner product space, two non-zero vectors with a positive dot product are linearly independent.
|
Orientation.cos_oangle_eq_inner_div_norm_mul_norm
theorem Orientation.cos_oangle_eq_inner_div_norm_mul_norm :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
x ≠ 0 → y ≠ 0 → (o.oangle x y).cos = ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)
This theorem states that in a real 2-dimensional inner product space with a specified orientation, the cosine of the oriented angle between two nonzero vectors is equal to their inner product divided by the product of their norms. In other words, if we have two nonzero vectors 'x' and 'y' in such a space, then the cosine of the angle between them as determined by the given orientation is calculated as the inner product of 'x' and 'y' divided by the product of the norms of 'x' and 'y'.
More concisely: In a real 2-dimensional inner product space with a specified orientation, the cosine of the angle between two nonzero vectors x and y is equal to their inner product x.y / (||x|| * ||y||).
|
Orientation.oangle_sign_sub_left
theorem Orientation.oangle_sign_sub_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
(o.oangle (x - y) y).sign = (o.oangle x y).sign
The theorem `Orientation.oangle_sign_sub_left` states that for any real inner product space `V` of finite dimension 2, given any orientation `o` of `V` and any two vectors `x` and `y` in `V`, the sign of the oriented angle `o.oangle` between the vector obtained by subtracting `y` from `x` and the vector `y` is the same as the sign of the oriented angle between `x` and `y`. This implies that subtracting the second vector from the first does not alter the sign of the oriented angle between them.
More concisely: For any orientation `o` of a 2-dimensional real inner product space `V` and vectors `x` and `y` in `V`, the sign of the oriented angle between `x - y` and `y` equals the sign of the oriented angle between `x` and `y`.
|
Orientation.oangle_sign_sub_right_swap
theorem Orientation.oangle_sign_sub_right_swap :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
(o.oangle y (y - x)).sign = (o.oangle x y).sign
This theorem states that in a real inner product space of finite rank 2, subtracting the first vector from the second vector and then swapping the vectors does not change the sign of their oriented angle. In other words, for any orientation `o` and vectors `x` and `y`, the sign of the oriented angle of `y` and `y - x` is equal to the sign of the oriented angle of `x` and `y`. This is analogous to saying in 2D geometry that subtracting a vector from another and then swapping the vectors does not change the sign of their angle.
More concisely: In a real inner product space of finite rank 2, the sign of the oriented angle between two vectors is preserved under vector subtraction and swapping.
|
Orientation.eq_iff_oangle_eq_zero_of_norm_eq
theorem Orientation.eq_iff_oangle_eq_zero_of_norm_eq :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
‖x‖ = ‖y‖ → (x = y ↔ o.oangle x y = 0)
The theorem states that for a real inner product space `V` of finite dimension equal to 2 and given an orientation `o` of `V`, for any two vectors `x` and `y` in `V`, if their norms are equal (`‖x‖ = ‖y‖`), then `x` is equal to `y` if and only if the oriented angle `o.oangle` between `x` and `y` is zero. In simpler terms, in a two-dimensional real inner product space, two vectors of the same length are identical if and only if the oriented angle between them is zero.
More concisely: In a 2-dimensional real inner product space with fixed orientation, two vectors with equal norms are equal if and only if they form a zero-degree angle with respect to the orientation.
|
Orientation.oangle_sign_sub_left_eq_neg
theorem Orientation.oangle_sign_sub_left_eq_neg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
(o.oangle (y - x) y).sign = -(o.oangle x y).sign
This theorem states that in a real inner product space `V` of dimension `2`, for any orientation `o` of the space and any two vectors `x` and `y` in the space, the sign of the angle (in the orientation `o`) obtained by subtracting the first vector `x` from the second vector `y` is the negation of the sign of the angle between vectors `x` and `y` in the orientation `o`. This is a property relating subtraction of vectors and the orientation of the angle between them.
More concisely: In a real inner product space of dimension 2, the angle between vectors x and y, and the angle between y and (x - y), have opposing signs in the same orientation.
|
Orientation.oangle_neg_left_eq_neg_right
theorem Orientation.oangle_neg_left_eq_neg_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
o.oangle (-x) y = o.oangle x (-y)
This theorem, `Orientation.oangle_neg_left_eq_neg_right`, states that for any normed additive commutative group `V` which also forms an inner product space over the real numbers `ℝ` and has a finite rank of 2, for any orientation `o` of this space, and any two vectors `x` and `y` in this space, the angle (`o.oangle`) between the negation of the first vector (`-x`) and the second vector `y` is equal to the angle between the first vector `x` and the negation of the second vector (`-y`). In other words, negating either vector does not change the angle between them.
More concisely: For any normed additive commutative 2-dimensional inner product space over the real numbers, and for any orientation and vectors x, y, the angle between -x and y equals the angle between x and -y.
|
Orientation.two_zsmul_oangle_right_of_span_eq
theorem Orientation.two_zsmul_oangle_right_of_span_eq :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) {y z : V},
Submodule.span ℝ {y} = Submodule.span ℝ {z} → 2 • o.oangle x y = 2 • o.oangle x z
This theorem states that in a real inner product space V of finite dimension 2, given an orientation `o` of `V` and a vector `x` in `V`, if the spans of two other vectors `y` and `z` in `V` are equal, then the double of the angle formed between `x` and `y` with respect to the orientation `o` equals the double of the angle formed between `x` and `z` with respect to the same orientation `o`. In other words, doubling the angle doesn't change it when the vectors `y` and `z` span the same subspace.
More concisely: In a real inner product space of finite dimension 2 with orientation `o`, the angle between a vector `x` and the span of vectors `y` and `z` (with respect to `o`) is equal to the angle between `x` and any vector in the span of `y` and `z` (also with respect to `o`). Therefore, the double of the angle formed between `x` and `y` (or `z`) is equal.
|
Orientation.ne_of_oangle_ne_zero
theorem Orientation.ne_of_oangle_ne_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y ≠ 0 → x ≠ y
This theorem states that in a two-dimensional real inner product space, if the oriented angle between two vectors is non-zero, then the two vectors are not equal. In other words, any two vectors with a non-zero oriented angle between them must be distinct vectors. This is valid for any given orientation of the space.
More concisely: In a two-dimensional real inner product space, two non-zero vectors with a non-zero oriented angle between them are distinct.
|
Orientation.oangle_sign_sub_left_swap
theorem Orientation.oangle_sign_sub_left_swap :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
(o.oangle (x - y) x).sign = (o.oangle x y).sign
The theorem `Orientation.oangle_sign_sub_left_swap` states that for any normed add commutative group `V` equipped with an inner product space over the real numbers, and having finite rank 2, given an orientation `o` of `V` and two vectors `x` and `y` in `V`, the sign of the angle obtained by subtracting `y` from `x` and then using `x` as reference, is equal to the sign of the angle between `x` and `y` in the given orientation. This asserts an invariance property for the sign of the angle under the operation of subtracting the second vector from the first and then swapping the vectors.
More concisely: For any finite rank 2 inner product space over the real numbers with orientation, the sign of the angle between two vectors is equal to the sign of the angle obtained by subtracting one from the other and swapping their order.
|
Orientation.oangle_sign_add_right
theorem Orientation.oangle_sign_add_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
(o.oangle x (x + y)).sign = (o.oangle x y).sign
This theorem states that, regardless of the orientation of a real, finite two-dimensional vector space, the sign of the oriented angle from a vector `x` to the vector `x + y` is identical to the sign of the oriented angle from `x` to `y`. In simpler terms, adding a vector `x` to another vector `y` does not change the sign of the angled orientation from `x` to `y`. This theorem is significant in the field of inner product spaces and vector orientations.
More concisely: The oriented angle from a vector `x` to `y` is equal in sign to the oriented angle from `x` to `(x + y)`.
|
Orientation.oangle_add_cyc3_neg_left
theorem Orientation.oangle_add_cyc3_neg_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y z : V},
x ≠ 0 → y ≠ 0 → z ≠ 0 → o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = ↑Real.pi
This theorem states that given a 2-dimensional real inner product space and three nonzero vectors in that space, if we add the oriented angles between each pair of vectors in a cyclic order, with the first vector in each angle negated, the result will be equal to π. This is an extension of the geometric concept of the sum of angles in a triangle, applied to the case where the sum of the vectors is zero.
More concisely: Given a 2-dimensional real inner product space and three nonzero vectors in it, the sum of the negated oriented angles between each pair in a cyclic order is equal to π.
|
Orientation.oangle_smul_left_of_pos
theorem Orientation.oangle_smul_left_of_pos :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) {r : ℝ},
0 < r → o.oangle (r • x) y = o.oangle x y
This theorem asserts that, given an orientation `o` of a vector space `V` (which is a normed add commutative group and an inner product space over the real numbers, and has a finite rank of 2), and given two vectors `x` and `y` in `V`, if `r` is a positive real number, then the oriented angle between `r*x` and `y` is the same as the oriented angle between `x` and `y`. In other words, scaling the first vector by a positive scalar does not change the oriented angle between two vectors.
More concisely: Given an orientation and a finite-dimensional real inner product space V, the oriented angle between x and y is equal to the oriented angle between rx and y for any positive real number r and vectors x, y in V.
|
Orientation.oangle_rev
theorem Orientation.oangle_rev :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
o.oangle y x = -o.oangle x y
The theorem `Orientation.oangle_rev` states that for a 2D vector space `V` with a real inner product and a given orientation `o`, swapping the order of the two vectors `x` and `y` in the `oangle` (oriented angle) function results in the negation of the original angle. In other words, the oriented angle from `y` to `x` is the negative of the oriented angle from `x` to `y`.
More concisely: For a 2D vector space equipped with a real inner product and orientation, the oriented angle from vector `y` to vector `x` is the negative of the oriented angle from vector `x` to vector `y`.
|
Orientation.inner_rev_eq_zero_of_oangle_eq_neg_pi_div_two
theorem Orientation.inner_rev_eq_zero_of_oangle_eq_neg_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(-Real.pi / 2) → ⟪y, x⟫_ℝ = 0
This theorem states that if the spatial orientation of two vectors results in an oriented angle of negative pi halves (i.e., -π/2), then the inner product of the two vectors, when their order is reversed, is zero. This theorem applies within a 2-dimensional inner product space over the real numbers. The spatial orientation of the vectors is defined in terms of the `Orientation` type, which represents the orientation of a module. The inner product is represented by the `⟪y, x⟫_ℝ` symbol.
More concisely: If the spatial orientation of two vectors in a 2-dimensional real inner product space results in an oriented angle of negative pi/2, then their reversed inner product is zero.
|
Orientation.oangle_neg_right
theorem Orientation.oangle_neg_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
x ≠ 0 → y ≠ 0 → o.oangle x (-y) = o.oangle x y + ↑Real.pi
This theorem, `Orientation.oangle_neg_right`, states that for any real inner product space `V` of finite rank 2, and any orientation `o` of `V`, if we take two non-zero vectors `x` and `y` in `V`, then the oriented angle between `x` and the negation of `y` (i.e., `-y`) is the same as the oriented angle between `x` and `y` plus π. Here, `π` is defined as twice a zero of cos in [1,2].
More concisely: For any real inner product space of finite rank 2 with orientation, the oriented angle between a vector and its negation is the sum of the oriented angles between that vector and the original vector and π.
|
Orientation.oangle_add_cyc3_neg_right
theorem Orientation.oangle_add_cyc3_neg_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y z : V},
x ≠ 0 → y ≠ 0 → z ≠ 0 → o.oangle x (-y) + o.oangle y (-z) + o.oangle z (-x) = ↑Real.pi
This theorem, `Orientation.oangle_add_cyc3_neg_right`, states that for any three nonzero vectors in a real inner product space of finite dimension 2, if you add the angles between these vectors in a cyclic order, negating the second vector in each angle, the sum equals π (or pi, approximately 3.14159). Here, the angle is determined with respect to a given orientation of the vector space. If the sum of the vectors equals zero, this is essentially stating the geometric fact that the sum of the angles in a triangle equals π.
More concisely: In a real inner product space of finite dimension 2, the sum of the counterclockwise angles between any three nonzero vectors, with the second vector negated in each angle, equals π.
|
Orientation.right_ne_zero_of_oangle_eq_neg_pi_div_two
theorem Orientation.right_ne_zero_of_oangle_eq_neg_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(-Real.pi / 2) → y ≠ 0
This theorem states that for any two vectors `x` and `y` in a two-dimensional real inner product space `V`, given an orientation `o` of the space, if the oriented angle from `x` to `y` according to `o` is `-π/2`, then the vector `y` cannot be the zero vector. In other words, if the angle between two vectors is `-π/2`, the second vector is non-zero.
More concisely: In a two-dimensional real inner product space, if the oriented angle between vectors `x` and `y` according to an orientation `o` is `-π/2`, then `y` is a non-zero vector.
|
Orientation.oangle_smul_left_of_neg
theorem Orientation.oangle_smul_left_of_neg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) {r : ℝ},
r < 0 → o.oangle (r • x) y = o.oangle (-x) y
The theorem `Orientation.oangle_smul_left_of_neg` states that for any real normed add-commutative group `V` with an inner product space over the real numbers, given that the rank of `V` is 2 and fixed `o` as an orientation of `V`, for any vectors `x` and `y` in `V` and a real number `r` less than zero, the oriented angle `o.oangle` of the vector obtained by scaling `x` by `r` with `y` is the same as the oriented angle of the negated vector `-x` with `y`. This means that multiplying the first vector in the oriented angle by a negative real number is equivalent to negating the vector in terms of the resulting angle.
More concisely: For any 2-dimensional real normed add-commutative group with inner product and orientation, the oriented angle between a vector and another vector is equal to the oriented angle between the negation of the first vector and the second vector, when the scalar multiplication is performed with a negative real number.
|
Orientation.oangle_map
theorem Orientation.oangle_map :
∀ {V : Type u_1} {V' : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedAddCommGroup V']
[inst_2 : InnerProductSpace ℝ V] [inst_3 : InnerProductSpace ℝ V']
[inst_4 : Fact (FiniteDimensional.finrank ℝ V = 2)] [inst_5 : Fact (FiniteDimensional.finrank ℝ V' = 2)]
(o : Orientation ℝ V (Fin 2)) (x y : V') (f : V ≃ₗᵢ[ℝ] V'),
((Orientation.map (Fin 2) f.toLinearEquiv) o).oangle x y = o.oangle (f.symm x) (f.symm y)
This theorem, `Orientation.oangle_map`, states that the angle between two vectors in a real normed add-commutative group with an inner product space structure, when considered with respect to an orientation created by a map with a linear isometric equivalence, is identical to the angle between those two vectors transformed by the inverse of that isometric equivalence, with respect to the original orientation. The theorem applies to spaces of finite rank 2, and uses the `Orientation.map` function, which maps orientations under module equivalences, and the `oangle` function, which computes the angle between vectors given an orientation.
More concisely: In a real normed add-commutative group with an inner product space structure and finite rank 2, the angle between two vectors, with respect to an orientation created by a linear isometric equivalence, is equal to the angle between those vectors transformed by the inverse of that isometric equivalence, with respect to the original orientation.
|
Orientation.oangle_neg_neg
theorem Orientation.oangle_neg_neg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
o.oangle (-x) (-y) = o.oangle x y
The theorem `Orientation.oangle_neg_neg` states that for any vector space `V` that is also a normed add commutative group and an inner product space over the real numbers, with a dimension of 2, and for any orientation `o` of `V`, the angle between the negation of two vectors `x` and `y` (denoted by `o.oangle (-x) (-y)`) is equal to the angle between the vectors `x` and `y` (denoted by `o.oangle x y`). In simpler terms, negating both vectors in a two-dimensional real inner product space does not change the angle between them.
More concisely: In a 2-dimensional real inner product space with orientation, the angle between the negations of two vectors is equal to the angle between the original vectors.
|
Orientation.ne_of_oangle_eq_neg_pi_div_two
theorem Orientation.ne_of_oangle_eq_neg_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(-Real.pi / 2) → x ≠ y
This theorem states that if the angle between two vectors in a real inner product space of finite rank 2 is negative half of the mathematical constant Pi (i.e., `-π / 2`), then those two vectors are not equal to each other. In other words, in a 2-dimensional real vector space, no two distinct vectors can have an angle of `-π / 2` between them.
More concisely: In a real inner product space of finite rank 2, two distinct vectors do not have an angle of negative half-pi between them.
|
Orientation.oangle_smul_right_of_pos
theorem Orientation.oangle_smul_right_of_pos :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) {r : ℝ},
0 < r → o.oangle x (r • y) = o.oangle x y
The theorem `Orientation.oangle_smul_right_of_pos` states that for an oriented 2-dimensional real inner product space `V`, multiplying the second vector passed to the orientation angle function `o.oangle` by a positive real number `r` does not change the angle. In other words, if `x` and `y` are vectors in `V`, `o` is an orientation of `V`, and `r` is a positive real number, then the angle `o.oangle x (r • y)` is equal to `o.oangle x y`. This theorem asserts the scaling invariance of the angle between two vectors with respect to the second vector.
More concisely: For an oriented 2-dimensional real inner product space and vectors x, y with positive real scalar r, the orientation angle of x with respect to r*y is equal to the orientation angle of x with respect to y.
|
Orientation.left_ne_zero_of_oangle_ne_zero
theorem Orientation.left_ne_zero_of_oangle_ne_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y ≠ 0 → x ≠ 0
The theorem `Orientation.left_ne_zero_of_oangle_ne_zero` states that for a 2-dimensional real inner product space, if the oriented angle between two vectors is not zero, then the first vector must be non-zero. This is equivalent to saying that if a vector forms a non-zero angle with another vector, then it cannot be the zero vector.
More concisely: If the oriented angle between two vectors in a 2-dimensional real inner product space is non-zero, then each vector is non-zero.
|
Orientation.right_ne_zero_of_oangle_sign_ne_zero
theorem Orientation.right_ne_zero_of_oangle_sign_ne_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
(o.oangle x y).sign ≠ 0 → y ≠ 0
This theorem states that in a real inner product space `V`, which is a normed add commutative group and has a finite dimension equal to 2, if the sign of the oriented angle between two vectors `x` and `y` according to a given orientation `o` is not zero, then the vector `y` cannot be the zero vector. In other words, if `x` and `y` are not orthogonal according to the orientation `o`, `y` must be non-zero.
More concisely: In a 2-dimensional real inner product space, if the oriented angle between two non-orthogonal vectors is non-zero, then neither vector is the zero vector.
|
Orientation.abs_oangle_sub_right_toReal_lt_pi_div_two
theorem Orientation.abs_oangle_sub_right_toReal_lt_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
‖x‖ = ‖y‖ → |(o.oangle x (x - y)).toReal| < Real.pi / 2
This theorem, named `Orientation.abs_oangle_sub_right_toReal_lt_pi_div_two`, states that in a two-dimensional inner product space over the real numbers, given an orientation and two vectors `x` and `y` of the same magnitude, the absolute value of the oriented angle from `x` to `x - y` is less than $\pi / 2$. This corresponds to the geometric fact that a base angle of an isosceles triangle is acute. The orientation and the fact that we are working in a two-dimensional space are necessary to give meaning to the notion of angle in the context of a general inner product space.
More concisely: In a 2-dimensional real inner product space with given orientation, the absolute value of the oriented angle between vectors `x` and `x - y` is less than $\pi / 2$, given `x` and `y` of equal magnitudes.
|
Orientation.oangle_sign_sub_right
theorem Orientation.oangle_sign_sub_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
(o.oangle x (y - x)).sign = (o.oangle x y).sign
This theorem, `Orientation.oangle_sign_sub_right`, states that for any real inner product space `V` of dimension 2, given any orientation `o` of this space, and any two vectors `x` and `y` from this space, the sign of the angle `o.oangle` between `x` and the vector resulting from subtracting `x` from `y` is equal to the sign of the angle `o.oangle` between `x` and `y`. In other words, subtracting the first vector from the second does not change the sign of the angle between them in this context.
More concisely: For any orientation `o` of a 2-dimensional real inner product space `V` and vectors `x` and `y` in `V`, the sign of the angle between `x` and `y` is equal to the sign of the angle between `x` and `(y - x)`.
|
Orientation.oangle_sign_smul_add_smul_smul_add_smul
theorem Orientation.oangle_sign_smul_add_smul_smul_add_smul :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) (r₁ r₂ r₃ r₄ : ℝ),
(o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign
This theorem states that for a 2-dimensional real inner product space `V` with a given orientation `o`, and for any two vectors `x` and `y` in this space and any four real numbers `r₁`, `r₂`, `r₃`, and `r₄`, the sign of the angle between the linear combinations `r₁ • x + r₂ • y` and `r₃ • x + r₄ • y` is equal to the product of the sign of the determinant of the matrix formed by `r₁`, `r₂`, `r₃`, and `r₄` (i.e., `r₁ * r₄ - r₂ * r₃`), and the sign of the angle between the vectors `x` and `y`.
More concisely: The sign of the inner product of linear combinations of vectors x and y is equal to the product of the determinant's sign and the sign of the angle between x and y.
|
Orientation.oangle_neg_self_right
theorem Orientation.oangle_neg_self_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V},
x ≠ 0 → o.oangle x (-x) = ↑Real.pi
The theorem `Orientation.oangle_neg_self_right` states that for a vector space `V` over the real numbers ℝ, which has a norm and an inner product, and is two-dimensional, the angle between any non-zero vector `x` and its negation `-x`, according to any given orientation `o` of `V`, is equal to π. This basically restates the geometric fact that a vector and its negation, in a two-dimensional space, point in exactly opposite directions, and so the angle between them is π radians.
More concisely: In a two-dimensional real vector space equipped with a norm and inner product, the angle between a non-zero vector and its negation, according to any orientation, is equal to π radians.
|
Orientation.two_zsmul_oangle_smul_left_of_ne_zero
theorem Orientation.two_zsmul_oangle_smul_left_of_ne_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) {r : ℝ},
r ≠ 0 → 2 • o.oangle (r • x) y = 2 • o.oangle x y
The theorem `Orientation.two_zsmul_oangle_smul_left_of_ne_zero` states that for a given real vector space `V` with a normed addative commutative group structure and an inner product space structure, and with a fixed orientation `o` and finite dimension equal to 2, if we have two vectors `x` and `y` and a nonzero real number `r`, then the angle between the vector `r • x` and `y` times 2 (scaled by 2) is the same as the angle between `x` and `y` also scaled by 2. In essence, this theorem describes the property of angle invariance under scaling by a nonzero scalar in a 2-dimensional real inner product space.
More concisely: In a 2-dimensional real inner product space with a fixed orientation and a normed additive commutative group structure, the angle between vectors `x` and `y` is equal to the angle between `r • x` and `2 * y` for any nonzero real number `r`.
|
Orientation.oangle_sign_smul_sub_right
theorem Orientation.oangle_sign_smul_sub_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) (r : ℝ),
(o.oangle x (r • x - y)).sign = -(o.oangle x y).sign
The theorem `Orientation.oangle_sign_smul_sub_right` states that for any real vector space `V` of finite rank 2, given an orientation `o` of `V` and any two vectors `x` and `y` in `V`, and a real number `r`, the sign of the "angle" (as defined by the method `oangle` of the orientation `o`) between `x` and the vector obtained by subtracting `y` from the scalar multiple `r` of `x`, is the negative of the sign of the "angle" between `x` and `y`. In simpler terms, subtracting a vector `y` from a scalar multiple of another vector `x` switches the orientation of the angle between `x` and `y`.
More concisely: For any orientation `o` of a finite rank 2 real vector space `V`, and vectors `x`, `y` in `V` and real number `r`, the sign of `oangle(o, x, r*x - y)` is the negative of the sign of `oangle(o, x, y)`.
|
Orientation.left_ne_zero_of_oangle_sign_eq_one
theorem Orientation.left_ne_zero_of_oangle_sign_eq_one :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
(o.oangle x y).sign = 1 → x ≠ 0
This theorem states that given a 2-dimensional real inner product space `V` with a chosen orientation `o`, if the sign of the oriented angle between two vectors `x` and `y` is `1`, then the first vector `x` is not the zero vector. In simple terms, if two vectors in a 2D space are oriented such that they form a positive angle with respect to the chosen orientation, then the starting vector must not be a zero vector.
More concisely: In a 2-dimensional real inner product space with a chosen orientation, if the oriented angle between two vectors is positive, then neither vector is the zero vector.
|
Orientation.two_zsmul_oangle_left_of_span_eq
theorem Orientation.two_zsmul_oangle_left_of_span_eq :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V} (z : V),
Submodule.span ℝ {x} = Submodule.span ℝ {y} → 2 • o.oangle x z = 2 • o.oangle y z
This theorem states that in a real inner product space of finite dimension 2, given an orientation and three vectors x, y, z, if the submodules spanned by vectors x and y are equal, then the doubled angles formed by vectors x, z and y, z (with x and y on the left respectively) under the given orientation are also equal.
More concisely: In a 2-dimensional real inner product space with a fixed orientation, if the subspaces spanned by vectors x and y are equal, then the angles formed by x, z, and y, z (with x and y on the left, respectively) under the given orientation are congruent.
|
Orientation.oangle_zero_right
theorem Orientation.oangle_zero_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V), o.oangle x 0 = 0
This theorem, `Orientation.oangle_zero_right`, states that for any vector `x` in a two-dimensional real vector space `V`, if we take the oriented angle `o.oangle` between `x` and the zero vector, the result is always zero. This holds true regardless of the particular orientation `o` of the vector space. The vector space `V` is assumed to be a normed add commutative group and an inner product space over the field of real numbers.
More concisely: For any vector `x` in a two-dimensional real inner product space `V`, the oriented angle between `x` and the zero vector is 0.
|
Orientation.oangle_neg_orientation_eq_neg
theorem Orientation.oangle_neg_orientation_eq_neg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
(-o).oangle x y = -o.oangle x y
This theorem states that for any orientation `o`, and any vectors `x` and `y` in a two-dimensional real inner product space `V`, the oriented angle from `x` to `y` under the negation of `o` is the negation of the oriented angle from `x` to `y` under `o`. In other words, negating the orientation effectively reverses the direction in which angles are measured.
More concisely: For any orientation `o` and vectors `x` and `y` in a 2-dimensional real inner product space, the oriented angle from `x` to `y` under the negation of `o` is the negation of the oriented angle from `x` to `y` under `o`.
|
Orientation.oangle_sign_smul_add_smul_right
theorem Orientation.oangle_sign_smul_add_smul_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) (r₁ r₂ : ℝ),
(o.oangle x (r₁ • x + r₂ • y)).sign = SignType.sign r₂ * (o.oangle x y).sign
This theorem states that in a real inner product space `V` of dimension 2, given an orientation `o`, two vectors `x` and `y`, and two real factors `r₁` and `r₂`, the sign of the oriented angle between vector `x` and the vector formed by the linear combination `r₁ • x + r₂ • y` is equal to the product of the sign of `r₂` and the sign of the oriented angle between `x` and `y`. In other words, the sign of the angle between a vector and a linear combination of that vector with a second vector is the product of the sign of the factor multiplying the second vector in the combination and the sign of the angle between the two vectors.
More concisely: In a real inner product space of dimension 2 with given orientation, the sign of the angle between a vector and its linear combination with another vector is equal to the product of the sign of the coefficient of the second vector and the sign of the angle between the original vectors.
|
Orientation.ne_of_oangle_sign_eq_neg_one
theorem Orientation.ne_of_oangle_sign_eq_neg_one :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
(o.oangle x y).sign = -1 → x ≠ y
This theorem states that for a 2-dimensional real vector space `V` having an orientation `o`, if the sign of the oriented angle `o.oangle` between two vectors `x` and `y` in `V` is `-1`, then the vectors `x` and `y` must be distinct, they cannot be equal. This is a property related to the geometric interpretation of vectors in a 2-dimensional space, where a negative angle indicates a direction reversal, implying that the vectors cannot be the same.
More concisely: In a 2-dimensional real vector space with orientation, if the oriented angle between two vectors is negative, then the vectors are linearly independent and not equal.
|
Orientation.oangle_add_swap
theorem Orientation.oangle_add_swap :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y z : V},
x ≠ 0 → y ≠ 0 → z ≠ 0 → o.oangle y z + o.oangle x y = o.oangle x z
This theorem states that for any three non-zero vectors `x`, `y`, and `z` in a 2-dimensional Euclidean vector space `V` with a given orientation `o`, the sum of the angle between vectors `y` and `z` and the angle between vectors `x` and `y` equals the angle between vectors `x` and `z`. Here, the angles are calculated with respect to the given orientation of the vector space.
More concisely: In a 2-dimensional Euclidean vector space with a given orientation, the angle between vectors `x` and `z` is equal to the sum of the angles between vectors `x` and `y`, and `y` and `z`.
|
Orientation.inner_eq_norm_mul_norm_mul_cos_oangle
theorem Orientation.inner_eq_norm_mul_norm_mul_cos_oangle :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V),
⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ * (o.oangle x y).cos
This theorem, named `Orientation.inner_eq_norm_mul_norm_mul_cos_oangle`, states that for a normed additive commutative group `V` which is an inner product space over the real numbers ℝ and has a rank of 2, for any orientation `o` of `V` and any two vectors `x` and `y` in `V`, the inner product of `x` and `y` is equal to the product of the norm of `x`, the norm of `y`, and the cosine of the oriented angle between `x` and `y` according to `o`. In mathematical terms, this can be written as ⟨x, y⟩ = ‖x‖ * ‖y‖ * cos(θ), where θ is the oriented angle between `x` and `y`.
More concisely: For any inner product space V of real dimension 2 with orientation o, the inner product of vectors x and y is equal to the product of their norms and the cosine of the oriented angle between them: ∥x∥ * ∥y∥ * cos(θo(x, y)).
|
Orientation.oangle_sign_smul_sub_left
theorem Orientation.oangle_sign_smul_sub_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x y : V) (r : ℝ),
(o.oangle (r • y - x) y).sign = -(o.oangle x y).sign
This theorem, `Orientation.oangle_sign_smul_sub_left`, states that for any real vector space 'V' with a normed additive commutative group structure and an inner product space over real numbers, having its finite rank equal to 2, any orientation 'o' of this vector space, and any two vectors 'x' and 'y' from this vector space and a real number 'r', the sign of the oriented angle between the vector obtained by subtracting 'x' from the vector obtained by scaling 'y' by 'r' and the vector 'y' is negative of the sign of the oriented angle between the vectors 'x' and 'y'. In other words, when we subtract the first vector from a scaled version of the second vector, the sign of the angle between these vectors is negated.
More concisely: For any 2-dimensional real vector space with a norm and inner product, and for any orientation, vectors x, y, and real number r, the sign of the oriented angle between y and the vector obtained by subtracting x from r*y is the negative of the sign of the angle between x and y.
|
Orientation.oangle_add
theorem Orientation.oangle_add :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y z : V},
x ≠ 0 → y ≠ 0 → z ≠ 0 → o.oangle x y + o.oangle y z = o.oangle x z
This theorem states that, for any inner product space of real numbers with a finite rank of 2 and a given orientation, given any three non-zero vectors, the sum of the oriented angles between the first and second vector and between the second and third vector is equal to the oriented angle between the first and third vector. In other words, this theorem confirms the angle addition property in a 2-dimensional real inner product space.
More concisely: In a 2-dimensional real inner product space with finite rank and given orientation, the sum of the angles between any pair of vectors is equal to the angle between the vectors forming a triangle.
|