Orientation.tan_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two
theorem Orientation.tan_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x + y) y).tan * ‖y‖ = ‖x‖
This theorem states that in the context of a normed additive commutative group `V` that also forms an inner product space over the real numbers, and further given that `V` has a finite dimension of 2, the orientation `o` applied to any two elements `x` and `y` of `V` such that the oriented angle `o.oangle x y` equals $\pi / 2$ (i.e., they are perpendicular), the tangent of the oriented angle between the sum of `x` and `y` and `y` multiplied by the norm of `y` equals the norm of `x`. This is essentially a formalization of the geometric fact that in a right-angled triangle, the tangent of an angle times the length of the adjacent side equals the length of the opposite side.
More concisely: In a 2-dimensional real inner product space, the norm of the difference of two perpendicular vectors is equal to the product of the tangent of their oriented angle and the norm of one vector.
|
Orientation.tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two
theorem Orientation.tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle y (y - x)).tan * ‖y‖ = ‖x‖
This theorem states that for any normed additive commutative group `V` equipped with a real inner product space structure, and given that the rank of `V` is 2, for any orientation `o` of `V` and any vectors `x` and `y` in `V`, if the oriented angle `o.oangle` between `x` and `y` equals pi/2 (which corresponds to a right angle in traditional geometry), then the tangent of the angled difference between `y` and `y - x`, multiplied by the norm of `y`, equals the norm of `x`. In other words, in a right-angled triangle, the tangent of the angle times the length of the adjacent side equals the length of the opposite side when considering the vectors `x` and `y` and the difference `y - x`.
More concisely: In a 2-dimensional real inner product space, given vectors `x` and `y` with right angle orientation `o`, the tangent of the angle between `y` and `y-x` equals the norm of `x`: tan(o.oangle(x, y)) = ||x||.
|
EuclideanGeometry.sin_oangle_right_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.sin_oangle_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
(EuclideanGeometry.oangle p₂ p₃ p₁).sin = dist p₁ p₂ / dist p₁ p₃
This theorem states that in a right-angled triangle in Euclidean geometry, if the angle at the second vertex (`p₂`) is π/2 radians (which corresponds to a right angle), then the sine of the angle at the first vertex (`p₁`) is equal to the ratio of the distance between the first and second vertices (`p₁` and `p₂`) to the distance between the first and third vertices (`p₁` and `p₃`). This theorem is formulated in the context of a 2-dimensional real inner product space.
More concisely: In a right-angled triangle in Euclidean geometry, the sine of the angle opposite the hypotenuse is equal to the ratio of the length of the leg adjacent to that angle to the length of the hypotenuse.
|
Orientation.oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two
theorem Orientation.oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → o.oangle y (y - x) = ↑(‖y‖ / ‖y - x‖).arccos
This theorem states that for a 2-dimensional real inner product space `V` with a given orientation `o`, and any two vectors `x` and `y` in `V`, if the oriented angle `o.oangle` between `x` and `y` is equal to π/2 (representing a right angle), then the oriented angle between `y` and the vector obtained by subtracting `x` from `y` equals the arc cosine of the ratio of the norm of `y` to the norm of `y - x`. This can be interpreted as expressing one of the angles in a right-angled triangle in terms of the arc cosine function when the two vectors `x` and `y` form a right angle with respect to the given orientation.
More concisely: For a 2-dimensional real inner product space with given orientation, the oriented angle between a vector `y` and the difference of `y` and a vector `x` forming a right angle is equal to the arc cosine of the dot product of `x` and `y` normalized by the product of their norms.
|
EuclideanGeometry.cos_oangle_left_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.cos_oangle_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
(EuclideanGeometry.oangle p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃
This theorem, 'EuclideanGeometry.cos_oangle_left_of_oangle_eq_pi_div_two', states that given a right-angled triangle in a Euclidean space of finite dimension 2, if the oriented angle ('oangle') at vertex p₂ (formed by the path from p₁ to p₂ to p₃) is equal to π/2 radians, then the cosine of the oriented angle formed at vertex p₁ (from p₃ to p₁ to p₂) is the ratio of the distance between points p₁ and p₂ to the distance between points p₁ and p₃. Here, the Euclidean Geometry, distances, and angles are defined within the structure of a normed add torsor and an inner product space over the real numbers.
More concisely: In a Euclidean space of finite dimension 2, the cosine of the angle at vertex p₁ in a right-angled triangle is equal to the ratio of the length of the side opposite p₁ to the length of the hypotenuse.
|
Orientation.norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two
theorem Orientation.norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → ‖y‖ / (o.oangle x (x + y)).sin = ‖x + y‖
This theorem states that in a right-angled triangle, the length of a side divided by the sine of the angle opposite to that side is equal to the length of the hypotenuse. More specifically, for a normed additive commutative group `V` with an inner product space over real numbers and having rank 2, given an orientation `o` and vectors `x` and `y` in `V` such that the oriented angle of `o` between vectors `x` and `y` is equal to pi/2 (representing a right angle), the theorem asserts that the norm of vector `y` divided by the sine of the oriented angle between vectors `x` and `x + y` is equal to the norm of the vector `x + y` (which represents the hypotenuse in the right-angled triangle formed by `x`, `y` and `x + y`).
More concisely: In a right-angled triangle with sides represented by vectors in a 2-dimensional inner product space over the real numbers, the ratio of the length of the hypotenuse to the length of the side opposing the right angle is equal to the sine of the angle between the two sides.
|
Orientation.oangle_add_left_smul_rotation_pi_div_two
theorem Orientation.oangle_add_left_smul_rotation_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V},
x ≠ 0 →
∀ (r : ℝ), o.oangle (x + r • (o.rotation ↑(Real.pi / 2)) x) (r • (o.rotation ↑(Real.pi / 2)) x) = ↑r⁻¹.arctan
The theorem `Orientation.oangle_add_left_smul_rotation_pi_div_two` states that for any 2-dimensional real inner product space V with a given orientation `o`, and any non-zero vector `x` in `V`, if another vector is defined by rotating `x` by an angle of π/2 radians and then scaling it by `r` (a real number), then the oriented angle between the vector `x + r * rotated_x` and the vector `r * rotated_x` equals the inverse tangent (arctan) of `r`. Here, `rotated_x` is the vector obtained by rotating `x` by π/2 radians.
More concisely: For any 2-dimensional real inner product space with orientation, and non-zero vector x, the oriented angle between x and r * (rotated_x), where rotated_x is the vector obtained by rotating x by π/2 radians, is equal to the inverse tangent of r.
|
EuclideanGeometry.cos_oangle_right_mul_dist_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.cos_oangle_right_mul_dist_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
(EuclideanGeometry.oangle p₂ p₃ p₁).cos * dist p₁ p₃ = dist p₃ p₂
This theorem states that in a two-dimensional oriented Euclidean space, given three points `p₁`, `p₂`, and `p₃`, if the oriented angle formed by `p₁`, `p₂`, and `p₃` is equal to `π/2` (or equivalently, a right angle), then the cosine of the oriented angle formed by `p₂`, `p₃`, and `p₁` multiplied by the distance from `p₁` to `p₃` equals the distance from `p₃` to `p₂`. This is essentially a restatement of the geometric fact that in a right-angled triangle, the length of the adjacent side is obtained by multiplying the length of the hypotenuse by the cosine of the angle.
More concisely: In a two-dimensional oriented Euclidean space, the cosine of the oriented angle between two vectors representing the segments from `p₁` to `p₂` and from `p₂` to `p₃`, multiplied by the length of the segment from `p₁` to `p₃`, equals the length of the segment from `p₃` to `p₂`.
|
EuclideanGeometry.dist_div_tan_oangle_right_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.dist_div_tan_oangle_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
dist p₁ p₂ / (EuclideanGeometry.oangle p₂ p₃ p₁).tan = dist p₃ p₂
This theorem states that for a right-angled triangle in a two-dimensional Euclidean space, the ratio of the distance between the first and second points (representing one side of the triangle) to the tangent of the angle at the second point (taken counter-clockwise from the line connecting the first and third points) is equal to the distance between the third and second points (representing the adjacent side to the angle). This is valid when the angle at the second point, when measured counterclockwise from the line segment connecting the first and third points, is equal to π/2 (or 90 degrees), which is indicative of a right-angled triangle. The Euclidean space is specified as a vector space over real numbers with an inner product and a norm, and is also equipped with the structure of a metric space and a normed add torsor.
More concisely: In a right-angled triangle in a 2-dimensional Euclidean space, the ratio of the length of the hypotenuse to the length of the side adjacent to the right angle is equal to the tangent of the angle between the hypotenuse and the side opposite the right angle.
|
Orientation.oangle_add_left_eq_arctan_of_oangle_eq_pi_div_two
theorem Orientation.oangle_add_left_eq_arctan_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → o.oangle (x + y) y = ↑(‖x‖ / ‖y‖).arctan
This theorem states that in a right-angled triangle, given an orientation of a 2-dimensional real inner product space, if the oriented angle between two vectors `x` and `y` is π/2 (i.e., they are orthogonal), then the oriented angle between the vector sum `x + y` and `y` is equal to the arctangent of the ratio of the norms of `x` and `y`. In other words, if `x` and `y` are perpendicular, the angle between `x + y` and `y` can be expressed using the `arctan` function applied to the ratio of their lengths.
More concisely: In a right-angled triangle of a 2-dimensional real inner product space, the angle between the sum of two orthogonal vectors `x` and `y`, and vector `y`, is equal to the arctangent of the norm ratio of `x` and `y`.
|
Orientation.sin_oangle_add_right_of_oangle_eq_pi_div_two
theorem Orientation.sin_oangle_add_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle x (x + y)).sin = ‖y‖ / ‖x + y‖
This theorem, named `Orientation.sin_oangle_add_right_of_oangle_eq_pi_div_two`, states that for any normed add commutative group `V` with an inner product space over the real numbers ℝ, and given that `V` has a finite rank of 2, for any orientation `o` of `V`, for any vectors `x` and `y` in `V`, if the oriented angle `o.oangle` between `x` and `y` is equal to π/2 (in radians), then the sine of the oriented angle between `x` and `x+y` is equal to the norm of `y` divided by the norm of `x+y`. In simpler words, it's basically a generalization of the result from trigonometry that in a right-angled triangle, the sine of an angle is the length of the opposite side divided by the length of the hypotenuse. Here, we are considering `x` and `y` as sides of a right-angled triangle in the 2-dimensional vector space, and `x+y` as the hypotenuse.
More concisely: For any 2-dimensional inner product space over the real numbers with orientation, if the oriented angle between two vectors is π/2, then the sine of the oriented angle between them and their sum is equal to the norm of the second vector divided by the norm of their sum.
|
Orientation.norm_div_tan_oangle_add_left_of_oangle_eq_pi_div_two
theorem Orientation.norm_div_tan_oangle_add_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → ‖x‖ / (o.oangle (x + y) y).tan = ‖y‖
This theorem states that for a right-angled triangle in a 2-dimensional real inner product space, if we have an orientation `o` such that the oriented angle `o.oangle x y` equals π/2 (90 degrees), then the length (`norm`) of the vector `x` divided by the tangent of the oriented angle `o.oangle (x + y) y` equals the length (`norm`) of the vector `y`. In other words, in this particular triangle, the ratio of the length of one side to the tangent of the angle at the opposite vertex equals the length of the adjoining side. This theorem applies mathematical concepts from trigonometry and linear algebra.
More concisely: In a right-angled triangle in a 2-dimensional real inner product space, the ratio of the length of one side to the tangent of the oriented angle at the opposite vertex equals the length of the adjacent side.
|
Orientation.oangle_sub_left_eq_arctan_of_oangle_eq_pi_div_two
theorem Orientation.oangle_sub_left_eq_arctan_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → o.oangle (x - y) x = ↑(‖y‖ / ‖x‖).arctan
This theorem states that for a normed add commutative group `V` with an inner product space over real numbers, having finite dimension equal to 2, and an orientation `o`, given two vectors `x` and `y` such that their oriented angle `o.oangle x y` is equal to π/2, the oriented angle between `x - y` and `x` is equal to the arctangent of the norm of `y` divided by the norm of `x`. In essence, this theorem is expressing the angle in a right-angled triangle using the arctangent function, where the triangle is formed by the vectors `x`, `y`, and `x - y`.
More concisely: For a 2-dimensional real inner product space `V` with orientation `o`, the oriented angle between `o.oangle (x - y) x` is equal to $\arctan\left(\frac{\|y\|}{\|x\|}\right)$, given `x` and `y` with oriented angle `π/2`.
|
Orientation.norm_div_cos_oangle_add_right_of_oangle_eq_pi_div_two
theorem Orientation.norm_div_cos_oangle_add_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → ‖x‖ / (o.oangle x (x + y)).cos = ‖x + y‖
This theorem states that for a right-angled triangle in a 2-dimensional real inner product space, if the orientation-formed angle between vectors `x` and `y` is π/2 (i.e., they are orthogonal), then the length (or norm) of vector `x` divided by the cosine of the angle between `x` and `x + y` equals the length of `x + y`. In simpler terms, if `x` and `y` form a right angle, then the hypotenuse of the triangle formed by `x`, `y`, and `x + y` is given by the magnitude of `x` divided by the cosine of the angle between `x` and `x + y`. This is a generalization of an elementary geometric fact about right triangles to the setting of real vector spaces.
More concisely: In a 2-dimensional real inner product space, if vectors `x` and `y` form a right angle, then the length of `x` divided by the cosine of the angle between `x` and `x + y` equals the length of `x + y`.
|
Orientation.sin_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two
theorem Orientation.sin_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x + y) y).sin * ‖x + y‖ = ‖x‖
This theorem states that for a 2-dimensional oriented real inner product space V, given an orientation `o` and vectors `x` and `y` such that the oriented angle `o.oangle x y` between `x` and `y` is equal to π/2 (that is, `x` and `y` are orthogonal), the sine of the oriented angle `(o.oangle (x + y) y)` between the vector sum `x + y` and `y`, when multiplied by the norm of the vector sum `x + y`, is equal to the norm of the vector `x`. Essentially, this provides a geometric interpretation of the sine function in the context of a right-angled triangle in vector space: it corresponds to the length of the side opposite to the angle, when the hypotenuse is used to scale the sine of the angle.
More concisely: In a 2-dimensional oriented real inner product space, the sine of the oriented angle between a vector and its orthogonal complement, when scaled by the norm of their sum, equals the norm of the original vector.
|
Orientation.tan_oangle_sub_left_of_oangle_eq_pi_div_two
theorem Orientation.tan_oangle_sub_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x - y) x).tan = ‖y‖ / ‖x‖
This theorem states that in a real inner product space V of finite dimension 2, given an orientation `o` of `V` and two vectors `x` and `y` in `V` such that the oriented angle `o.oangle x y` between `x` and `y` is π/2 (i.e., they are orthogonal), the tangent of the oriented angle between the vector `x - y` and `x` is equal to the ratio of the norm of `y` to the norm of `x`.
This corresponds to the geometric intuition in a right-angled triangle where the tangent of an angle is the ratio of the length of the side opposite to the angle (corresponding to `‖y‖`) to the length of the side adjacent to the angle (corresponding to `‖x‖`).
More concisely: In a real inner product space of finite dimension 2, the tangent of the oriented angle between vector `x` and `y`, where `x` and `y` are orthogonal, is equal to the ratio of the norm of `y` to the norm of `x`.
|
Orientation.oangle_add_left_eq_arcsin_of_oangle_eq_pi_div_two
theorem Orientation.oangle_add_left_eq_arcsin_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → o.oangle (x + y) y = ↑(‖x‖ / ‖x + y‖).arcsin
This theorem states that in a right-angled triangle formed in a two-dimensional vector space (`V`), given the orientation (`o`) of the space and two vectors (`x` and `y`) such that the angle between them is π/2 radians (which is a right angle), the angle between the vector resulting from the addition of `x` and `y` (`x + y`) and `y` is equivalent to the inverse sine (`arcsin`) of the ratio of the norm (length) of `x` to the norm of `x + y`. This theorem essentially expresses a specific angle in a right-angled triangle in terms of `arcsin`.
More concisely: In a right-angled triangle in a 2-dimensional vector space, the angle between the sum of two vectors and one vector is equal to the inverse sine of the ratio of the length of the first vector to the length of their sum.
|
Orientation.oangle_sub_left_eq_arcsin_of_oangle_eq_pi_div_two
theorem Orientation.oangle_sub_left_eq_arcsin_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → o.oangle (x - y) x = ↑(‖y‖ / ‖x - y‖).arcsin
This theorem states that for any real inner product space of finite dimension 2 with a specified orientation, if the oriented angle between two vectors `x` and `y` is π/2 (or equivalently, `x` and `y` are orthogonal), then the oriented angle between the vector `x - y` and `x` is equal to the arcsine of the ratio of the norm of `y` to the norm of `x - y`. This theorem can be seen as a mathematical representation of a geometric concept in a two-dimensional Euclidean space, where it interprets the angle in a right-angled triangle in terms of the arcsine function.
More concisely: In a 2-dimensional real inner product space with a specified orientation, the oriented angle between the difference of two orthogonal vectors and the first vector is equal to the arcsine of the ratio of the second vector's norm to the difference's norm.
|
Orientation.norm_div_sin_oangle_add_left_of_oangle_eq_pi_div_two
theorem Orientation.norm_div_sin_oangle_add_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → ‖x‖ / (o.oangle (x + y) y).sin = ‖x + y‖
This theorem states that in a right-angled triangle, if we have a vector space `V` over the real numbers `ℝ` with an inner product and it is two-dimensional, and `o` is an orientation of `V`, then for any vectors `x` and `y` in `V`, if the oriented angle `o.oangle` between `x` and `y` is equal to π/2 (which is the angle in radians corresponding to a right angle), then the ratio of the norm of `x` to the sine of the oriented angle between the vectors `x + y` and `y` is equal to the norm of the vector `x + y`.
In simpler terms, this theorem is another way of expressing one of the properties of a right-angled triangle in the context of vector spaces: if we divide the length of a side of such a triangle by the sine of the angle opposite that side, we get the length of the hypotenuse.
More concisely: In a two-dimensional real inner product space with given orientation, the ratio of the norm of a vector to the sine of the oriented angle between it and another vector is equal to the norm of their sum vector if and only if the oriented angle is a right angle.
|
Orientation.sin_oangle_sub_left_of_oangle_eq_pi_div_two
theorem Orientation.sin_oangle_sub_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x - y) x).sin = ‖y‖ / ‖x - y‖
This theorem states that for a 2-dimensional normed add-commutative group `V` equipped with an inner product space over the real numbers and a given orientation, if the oriented angle `o` between vectors `x` and `y` is pi/2 (which corresponds to a right angle), then the sine of the oriented angle between `x - y` and `x` is equal to the norm of `y` divided by the norm of `x - y`. This is akin to the trigonometric statement in a right-angled triangle where the sine of an angle is the ratio of the length of the opposite side to the length of the hypotenuse.
More concisely: For a 2-dimensional normed add-commutative group `V` with inner product over the real numbers and a given orientation, the sine of the oriented angle between `x` and `y` is equal to the norm of `y` divided by the norm of `x - y` when the oriented angle is pi/2.
|
EuclideanGeometry.oangle_left_eq_arctan_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.oangle_left_eq_arctan_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
EuclideanGeometry.oangle p₃ p₁ p₂ = ↑(dist p₃ p₂ / dist p₁ p₂).arctan
This theorem states that in a right-angled triangle in a 2-dimensional Euclidean space, if the angle at vertex $p₂$ (denoted as `EuclideanGeometry.oangle p₁ p₂ p₃`) is $\pi/2$ radians (i.e., it's a right angle), then the angle at vertex $p₁$ (denoted as `EuclideanGeometry.oangle p₃ p₁ p₂`) can be calculated by taking the inverse tangent (`arctan`) of the ratio of the distances between $p₃$ and $p₂$ and between $p₁$ and $p₂$. This is essentially an application of the tangent of an angle in a right-angled triangle, represented in terms of Euclidean geometry, inner product spaces, and oriented modules.
More concisely: In a right-angled triangle in a 2-dimensional Euclidean space, the angle opposite the right angle can be obtained as the inverse tangent of the ratio of the lengths of the legs.
|
Orientation.oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two
theorem Orientation.oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → o.oangle x (x + y) = ↑(‖y‖ / ‖x + y‖).arcsin
This theorem states that for any real-valued, 2-dimensional vector space with a given orientation, and any two vectors `x` and `y` in that space, if the oriented angle between `x` and `y` is π/2 (or equivalently, the vectors are orthogonal), then the oriented angle between `x` and the vector resulting from their addition is equal to the arcsine of the ratio of the norm of `y` to the norm of the sum of `x` and `y`. This property is a way of expressing an angle in a right triangle using `arcsin`.
More concisely: Given a real-dimensional vector space with orientation and vectors `x` and `y`, if `x` and `y` are orthogonal, then the oriented angle between `x` and their sum is equal to the arcsine of the quotient of `y`'s norm by the norm of `x + y`.
|
Orientation.oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two
theorem Orientation.oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → o.oangle x (x + y) = ↑(‖x‖ / ‖x + y‖).arccos
This theorem states that given a right-angled triangle in a 2-dimensional real inner product space, if the angle between vectors `x` and `y` is π/2 (indicating that it's a right angle), then the angle between vectors `x` and `x + y` is equal to the inverse cosine of the ratio of the norm of `x` to the norm of `x + y`. This theorem is particularly useful for expressing an angle in a right-angled triangle in terms of the `arccos` function.
More concisely: In a 2-dimensional real inner product space, the angle between vectors `x` and `x + y` in a right-angled triangle is equal to the inverse cosine of the norm ratio `|x|/|x + y|` of the hypotenuse and the leg `x`.
|
EuclideanGeometry.oangle_right_eq_arcsin_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.oangle_right_eq_arcsin_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
EuclideanGeometry.oangle p₂ p₃ p₁ = ↑(dist p₁ p₂ / dist p₁ p₃).arcsin
This theorem states that in a right-angled triangle (in a real inner product space of finite dimension 2), if the angle at a point is equal to pi/2 (indicating a right angle), then the angle at another point is equal to the arcsine of the ratio of distances from the first point to the other two points. More specifically, if the angle formed by points p₁, p₂, p₃ (in that order) is pi/2, then the angle formed by points p₂, p₃, p₁ (in this new order) is equal to the arcsine of the ratio of the distance from p₁ to p₂ to the distance from p₁ to p₃.
More concisely: In a right-angled triangle in a 2-dimensional real inner product space, the angle opposite the side with the shorter distance from the right angle is equal to the arcsine of the ratio of the length of the other side to it.
|
EuclideanGeometry.tan_oangle_right_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.tan_oangle_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
(EuclideanGeometry.oangle p₂ p₃ p₁).tan = dist p₁ p₂ / dist p₃ p₂
This theorem states that in the context of a right-angled triangle in a real two-dimensional inner product space, given three points `p₁`, `p₂`, and `p₃` such that the oriented angle `p₁ p₂ p₃` is equal to π/2 (which indicates that `p₂` is the vertex of the right angle), the tangent of the oriented angle `p₂ p₃ p₁` is equal to the ratio of the distances `p₁ p₂` to `p₃ p₂`. This corresponds to the geometric fact that in a right-angled triangle, the tangent of an angle is the ratio of the side opposite to the angle to the side adjacent to the angle.
More concisely: In a right-angled triangle in a real two-dimensional inner product space, the tangent of the angle opposite the right angle is equal to the ratio of the length of the hypotenuse to the length of the adjacent side.
|
EuclideanGeometry.oangle_right_eq_arctan_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.oangle_right_eq_arctan_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
EuclideanGeometry.oangle p₂ p₃ p₁ = ↑(dist p₁ p₂ / dist p₃ p₂).arctan
This theorem states that in the context of a right-angled triangle in a real inner product space of finite rank 2, if the oriented angle denoted by `EuclideanGeometry.oangle` at vertex `p₂` between edges `p₁p₂` and `p₃p₂` is equal to `π/2` (which characterizes a right angle), then the oriented angle at vertex `p₃` between edges `p₂p₃` and `p₁p₃` is equal to the arctangent of the ratio of the Euclidean distances `dist p₁ p₂` and `dist p₃ p₂`. In other words, in a right-angled triangle, if one of the angles is `π/2`, then another angle can be expressed as the arctangent of the ratio of the sides.
More concisely: In a right-angled triangle in a real inner product space of finite rank 2, the angle opposite the side with length the quotient of the lengths of the other two sides is given by the arctangent of their ratio.
|
EuclideanGeometry.oangle_left_eq_arccos_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.oangle_left_eq_arccos_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
EuclideanGeometry.oangle p₃ p₁ p₂ = ↑(dist p₁ p₂ / dist p₁ p₃).arccos
This theorem states that in a right-angled triangle with vertices in a normed additively torsioned metric space (essentially a geometrical space) of 2-dimensional real vector space, if the oriented angle at vertex `p₂` (denoted as `EuclideanGeometry.oangle p₁ p₂ p₃`), is equal to π/2 (or 90 degrees), then the oriented angle at vertex `p₁` (denoted as `EuclideanGeometry.oangle p₃ p₁ p₂`), will be equal to the inverse cosine (`arccos`) of the ratio of the distances from `p₁` to `p₂` and from `p₁` to `p₃`. This essentially describes the geometric relationship between the angles and sides in a right triangle in terms of trigonometric functions.
More concisely: In a right-angled triangle in a 2-dimensional real vector space with normed additively torsioned metric, the angle opposite the right angle equals the arccosine of the ratio of the lengths of the legs.
|
Orientation.tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two
theorem Orientation.tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle x (x + y)).tan * ‖x‖ = ‖y‖
The theorem `Orientation.tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two` states that for any real inner product space `V` of rank 2, and for any orientation `o` of `V`, given two vectors `x` and `y` in `V` such that the oriented angle `o.oangle` between `x` and `y` is π/2 (in radians), the tangent of the oriented angle between `x` and `x+y`, when multiplied by the norm of `x`, equals the norm of `y`. This is essentially a statement of the trigonometric rule for right-angled triangles in the context of a real inner product space.
More concisely: For any real inner product space of rank 2 with orientation `o`, if vectors `x` and `y` have an oriented angle of π/2, then tan(o.oangle(x, x+y)) * ||x|| = ||y||.
|
Orientation.oangle_add_left_eq_arccos_of_oangle_eq_pi_div_two
theorem Orientation.oangle_add_left_eq_arccos_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → o.oangle (x + y) y = ↑(‖y‖ / ‖x + y‖).arccos
This theorem states that for a right-angled triangle in a 2-dimensional inner product space over the real numbers with a given orientation, if the angle between two vectors `x` and `y` is π/2 (or equivalently, the vectors are perpendicular to each other), then the angle between the vector `x + y` and vector `y` equals the arccosine of the ratio of the norm of `y` to the norm of `x + y`. This is a generalization of a standard result from Euclidean geometry about the angles in a right-angled triangle.
More concisely: In a 2-dimensional real inner product space with given orientation, the angle between vectors `x` and `y`, and between `x + y` and `y`, is equal to the arccosine of the dot product of `x` and `y` divided by the product of their norms. (This holds when the angle between `x` and `y` is right-angled.)
|
EuclideanGeometry.dist_div_sin_oangle_right_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.dist_div_sin_oangle_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
dist p₁ p₂ / (EuclideanGeometry.oangle p₂ p₃ p₁).sin = dist p₁ p₃
This theorem states that in a right-angled triangle, the ratio of the length of one side to the sine of the angle opposite that side equals the length of the hypotenuse. More specifically, given a triangle defined by points p₁, p₂, and p₃ in a Euclidean space with an inner product (making it possible to measure angles and distances), if the angle at p₂ (between p₁-p₂ and p₂-p₃) is π/2 radians (i.e., a right angle), then the ratio of the distance from p₁ to p₂ to the sine of the angle at p₂ (between p₃-p₂ and p₂-p₁) is equal to the distance from p₁ to p₃. In other words, this is a formulation of the sine law specifically for right-angled triangles in 2-dimensional real vector spaces.
More concisely: In a right-angled triangle in a 2-dimensional Euclidean space, the ratio of the length of the side opposite the right angle to the sine of the right angle equals the length of the hypotenuse.
|
Orientation.sin_oangle_add_left_of_oangle_eq_pi_div_two
theorem Orientation.sin_oangle_add_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x + y) y).sin = ‖x‖ / ‖x + y‖
This theorem states that in a right-angled triangle in a two-dimensional real inner product space (i.e., a space equipped with a form of dot product), given two vectors `x` and `y` such that the angle between them as defined by a certain orientation equals π/2 (which means they are orthogonal), the sine of the angle between the vector `x + y` and the vector `y` is equal to the ratio of the norm (length) of `x` to the norm of `x + y`. This theorem essentially relates the ratios of the lengths of the sides of the right-angled triangle (formed by the vectors `x`, `y`, and `x + y`) to the sine of certain angles, in line with the geometric interpretation of the sine function.
More concisely: In a right-angled triangle in a two-dimensional real inner product space, the sine of the angle between vectors `x` and `x + y`, where `x` and `y` are orthogonal, is equal to the ratio of the norm of `x` to the norm of `x + y`.
|
Orientation.norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two
theorem Orientation.norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → ‖y‖ / (o.oangle y (y - x)).cos = ‖y - x‖
This theorem, `Orientation.norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two`, states that, for any oriented, real inner product space `V` of dimension 2 and any non-zero vectors `x` and `y` in `V`, if the oriented angle `o.oangle x y` between `x` and `y` is π/2 (which represents a right angle), then the norm (or length) of `y` divided by the cosine of the oriented angle between `y` and `y - x` is equal to the norm of `y - x`. This is essentially a generalization of the geometric property of right triangles that the length of the side adjacent to an angle, divided by the cosine of the angle, equals the length of the hypotenuse. Here, the vectors `y` and `y - x` form the sides of a right triangle, and the vector `x` forms the hypotenuse.
More concisely: Given an oriented 2-dimensional real inner product space and non-zero vectors x and y with oriented angle o.oangle x y = π/2, the norm of y is equal to the cosine of o.oangle (y, y - x) times the norm of y - x.
|
Orientation.cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two
theorem Orientation.cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle y (y - x)).cos * ‖y - x‖ = ‖y‖
This theorem states that in a real inner-product space `V` of finite dimension 2, given an orientation `o` and vectors `x` and `y` such that the oriented angle `o` between `x` and `y` is equal to π/2 (implying `x` and `y` are orthogonal), the cosine of the oriented angle between `y` and `y - x` (the vector directed from `x` to `y`) multiplied by the norm of `y - x` equals the norm of `y`. In terms of Euclidean geometry, this corresponds to the scenario of a right-angled triangle, where if `x` and `y` represent two perpendicular sides, the theorem asserts that the length of the side represented by `y` equals the cosine of the angle between `y` and the vector difference `y - x` times the length of `y - x`, which is the hypotenuse of the triangle.
More concisely: In a real inner-product space of finite dimension 2 with orientation and vectors `x`, `y`, if `x` and `y` are orthogonal, then the cosine of the angle between `y` and `y - x` times the norm of `y - x` equals the norm of `y`.
|
Orientation.cos_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two
theorem Orientation.cos_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle x (x + y)).cos * ‖x + y‖ = ‖x‖
This theorem is about the geometry of a right-angled triangle in a 2-dimensional real inner product space. It states that for any such space `V`, given an orientation `o` of `V`, if the oriented angle `o.oangle x y` between two vectors `x` and `y` in `V` is $\pi/2$ (90 degrees), then the cosine of the oriented angle `o.oangle x (x + y)` (between `x` and the vector sum `x + y`), multiplied by the norm (length) of `x + y`, equals the norm of `x`. This is essentially the statement of a geometric property about right-angled triangles: the cosine of one of the non-right angles, multiplied by the length of the hypotenuse, gives the length of the adjacent side.
More concisely: In a 2-dimensional real inner product space and for any given orientation, the cosine of the angle between a vector and the sum of that vector and another, multiplied by the norm of the sum, equals the norm of the first vector if and only if the angle between the vectors is a right angle.
|
Orientation.cos_oangle_sub_left_of_oangle_eq_pi_div_two
theorem Orientation.cos_oangle_sub_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x - y) x).cos = ‖x‖ / ‖x - y‖
This theorem states that for a two-dimensional real vector space `V` with norm and inner product, given an orientation `o` and two vectors `x` and `y` in `V`, if the oriented angle between `x` and `y` equals π/2 (which represents a right angle), then the cosine of the oriented angle between the vector difference `x - y` and `x` is equal to the ratio of the norm of `x` to the norm of `x - y`.
More concisely: For a two-dimensional real vector space equipped with a norm and inner product, the cosine of the oriented angle between vector `x` and `y`, with `x` and `y` having a right angle (oriented angle of π/2), is equal to the ratio of the norm of `x` to the norm of their difference.
|
Orientation.sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two
theorem Orientation.sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle y (y - x)).sin * ‖y - x‖ = ‖x‖
This theorem states that for any vectors `x` and `y` in a 2-dimensional real vector space `V` with an orientation `o`, if the oriented angle from `x` to `y` is equal to π/2 (90 degrees), then the sine of the oriented angle from `y` to `y - x` multiplied by the norm of the vector from `y` to `x` is equal to the norm of the vector `x`. In the context of a right-angled triangle, this can be interpreted as the length of the side opposite the right angle (represented by `x`) being equal to the hypotenuse (represented by `y - x`) multiplied by the sine of the angle between `y` and `y - x`.
More concisely: For any vectors `x` and `y` in a 2-dimensional real vector space with orientation `o`, if the oriented angle from `x` to `y` is π/2, then the norm of `x` equals the norm of `y - x` multiplied by the sine of that angle.
|
Orientation.oangle_sub_left_smul_rotation_pi_div_two
theorem Orientation.oangle_sub_left_smul_rotation_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V},
x ≠ 0 → ∀ (r : ℝ), o.oangle (x - r • (o.rotation ↑(Real.pi / 2)) x) x = ↑r.arctan
This theorem states that in a right-angled triangle within a 2-dimensional real inner product space, if one side of the triangle is a scaled rotation of another side by an angle of `π / 2` (90 degrees), then the angle of the triangle, expressed using the `arctan` function, is equal to the scaling factor. This is provided the vector representing one side of the triangle is not the zero vector. The rotation is defined in terms of the orientation of our 2-dimensional space.
More concisely: In a right-angled triangle in a 2-dimensional real inner product space, the cosine of the angle between two sides is equal to the ratio of the length of the shorter side to the length of the longer side.
|
Orientation.oangle_sub_right_smul_rotation_pi_div_two
theorem Orientation.oangle_sub_right_smul_rotation_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V},
x ≠ 0 →
∀ (r : ℝ), o.oangle (r • (o.rotation ↑(Real.pi / 2)) x) (r • (o.rotation ↑(Real.pi / 2)) x - x) = ↑r⁻¹.arctan
This theorem states that in a right-angled triangle, when one side is obtained by rotating another side by π/2 (90 degrees), the angle can be expressed using the arctan function. More specifically, given a module `V` equipped with a normed add commutative group structure and an inner product space structure over the real numbers, and an orientation `o` of this module (which is two-dimensional based on the assumption `hd2`), for any non-zero vector `x` in `V` and any real number `r`, the angle defined by the orientation `o` between `r` times the vector obtained by rotating `x` by π/2 using the orientation `o` and the difference of this rotated vector and `x` itself, is equal to the arctan of `1/r`. This is a geometric property that particularly applies to right-angled triangles in two-dimensional spaces.
More concisely: In a right-angled triangle with hypotenuse obtained by rotating one side by 90 degrees, the angle between the rotated side and the original side is given by the arctan of 1/the length of the rotated side.
|
EuclideanGeometry.oangle_left_eq_arcsin_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.oangle_left_eq_arcsin_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
EuclideanGeometry.oangle p₃ p₁ p₂ = ↑(dist p₃ p₂ / dist p₁ p₃).arcsin
This theorem states that in the context of a right-angled triangle in a 2-dimensional Euclidean space (whose points are represented in a normed add torsor and vectors are represented in an inner product space), if the angle at a point `p₂` between lines extending towards points `p₁` and `p₃` is π/2 (a right angle), then the angle at `p₁` between lines extending towards points `p₃` and `p₂` is equivalent to the arcsine of the ratio of the distance from `p₃` to `p₂` to the distance from `p₁` to `p₃`. In other words, it describes a relationship between an angle in a right-angled triangle and the arcsine of the ratio of the lengths of the sides opposite to and hypotenuse of the angle.
More concisely: In a right-angled triangle in a 2-dimensional Euclidean space, the angle opposite the side of length `d` is equal to the arcsine of `d / hypotenuse`.
|
EuclideanGeometry.tan_oangle_left_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.tan_oangle_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
(EuclideanGeometry.oangle p₃ p₁ p₂).tan = dist p₃ p₂ / dist p₁ p₂
This theorem, named `EuclideanGeometry.tan_oangle_left_of_oangle_eq_pi_div_two`, states that in a two-dimensional Euclidean space with a predefined orientation, for any three points `p₁`, `p₂`, and `p₃`, if the oriented angle `p₁ p₂ p₃` is equal to half of Pi (which corresponds to a right angle, or 90 degrees), then the tangent of the oriented angle `p₃ p₁ p₂` is equal to the ratio of the distance from `p₃` to `p₂` over the distance from `p₁` to `p₂`. This is a geometric interpretation of the tangent function in the context of a right-angled triangle formed by points `p₁`, `p₂`, and `p₃`.
More concisely: In a two-dimensional Euclidean space with a fixed orientation, the tangent of the angle opposite the right angle in a right-angled triangle is equal to the length of the leg adjacent to the right angle divided by the length of the hypotenuse.
|
EuclideanGeometry.sin_oangle_left_mul_dist_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.sin_oangle_left_mul_dist_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
(EuclideanGeometry.oangle p₃ p₁ p₂).sin * dist p₁ p₃ = dist p₃ p₂
This theorem states that given a right-angled triangle in a 2-dimensional oriented Euclidean geometry, if the oriented angle (`EuclideanGeometry.oangle`) made by points p₁, p₂, and p₃ is exactly π/2 (which corresponds to a right angle), then the sine of the oriented angle made by points p₃, p₁, and p₂ multiplied by the distance between points p₁ and p₃ equals the distance between points p₃ and p₂. In other words, in a right-angled triangle, the product of the length of the hypotenuse and the sine of one of the non-right angles equals the length of the side opposite that angle, which is a formulation of the sine rule.
More concisely: In a right-angled triangle, the product of the length of the hypotenuse and the sine of one of the non-right angles equals the length of the side opposite that angle.
|
Orientation.norm_div_cos_oangle_add_left_of_oangle_eq_pi_div_two
theorem Orientation.norm_div_cos_oangle_add_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → ‖y‖ / (o.oangle (x + y) y).cos = ‖x + y‖
This theorem states that for a real number inner product space with a dimension of 2 and any orientation, given two vectors `x` and `y` such that their oriented angle equals pi over 2 (which indicates a right angle), the norm of `y` divided by the cosine of the oriented angle between the vector `x + y` and `y` equals the norm of the vector `x + y`. In simpler terms, this is equivalent to saying that in a right-angled triangle, the length of a side adjacent to an angle, divided by the cosine of that angle, equals the length of the hypotenuse.
More concisely: In a 2-dimensional real inner product space with any orientation, the quotient of the norm of vector `y` by the cosine of the oriented angle between vectors `x` and `x + y`, where `x` and `y` form a right angle, equals the norm of vector `x + y`.
|
Orientation.cos_oangle_sub_right_of_oangle_eq_pi_div_two
theorem Orientation.cos_oangle_sub_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle y (y - x)).cos = ‖y‖ / ‖y - x‖
This theorem states that in a real inner product space of two dimensions with a given orientation, if the angle between two vectors `x` and `y` is π/2 (i.e., the vectors are orthogonal, forming a right-angled triangle), then the cosine of the angle formed by `y` and the vector resulting from subtracting `x` from `y` is equal to the ratio of the norm of `y` to the norm of the vector `y - x`. This is a geometric interpretation of the cosine function in terms of ratios of lengths of sides in a right-angled triangle.
More concisely: In a 2-dimensional real inner product space, the cosine of the angle between vectors `x` and `y` is equal to the quotient of the norm of `y` and the norm of `y - x` when `x` and `y` are orthogonal.
|
Orientation.norm_div_sin_oangle_sub_left_of_oangle_eq_pi_div_two
theorem Orientation.norm_div_sin_oangle_sub_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → ‖y‖ / (o.oangle (x - y) x).sin = ‖x - y‖
This theorem states that in the context of a normed add commutative group `V` which is also an inner product space over the real numbers `ℝ`, with the additional fact that the finite rank of `V` over `ℝ` equals 2, given an orientation `o` of `V` and vectors `x` and `y` in `V` such that the oriented angle `o.oangle x y` equals pi/2 (which corresponds to a right angle in trigonometry), the length (norm) of the vector `y` divided by the sine of the oriented angle `(o.oangle (x - y) x)` equals the length of the vector `x - y`. This corresponds to the trigonometric principle that in a right-angled triangle, the length of a side divided by the sine of its opposite angle equals the length of the hypotenuse. In this case, the vectors `x`, `y`, and `x - y` form a right-angled triangle in the vector space `V`.
More concisely: Given a 2-dimensional real inner product space `V` with orientation `o`, vectors `x` and `y` forming a right angle, the quotient of `y`'s length by the sine of the angle between `x` and `x-y` is equal to the length of `x-y`.
|
Orientation.norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two
theorem Orientation.norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → ‖x‖ / (o.oangle y (y - x)).tan = ‖y‖
This theorem states that for a right-angled triangle formed by vectors in a real inner product space of finite dimension two, if one vector makes an angle of π/2 with the orientation of the space, then the ratio of the norm (length) of this vector to the tangent of the angle between the other vector and the difference of the other vector and the first vector equals the norm of the other vector. Put simply, in a right-angled triangle, the length of a side divided by the tangent of the opposite angle equals the length of the adjacent side.
More concisely: In a right-angled triangle in a real inner product space of finite dimension two, the ratio of the norm of one vector forming a right angle to the space's orientation to the tangent of the angle between the other two vectors equals the norm of the other vector.
|
Orientation.sin_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two
theorem Orientation.sin_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle x (x + y)).sin * ‖x + y‖ = ‖y‖
This theorem says that in a 2-dimensional inner product space (which can be thought of as analogous to a plane in Euclidean geometry), given an orientation of the space and two vectors `x` and `y` such that the oriented angle between them is `π/2` (i.e., they are perpendicular), then the sine of the oriented angle between `x` and `x + y` (the vector sum of `x` and `y`) multiplied by the norm (length) of `x + y` is equal to the norm of `y`. In other words, this theorem is a version of the geometric fact from trigonometry that in a right-angled triangle, the length of the side opposite the right angle (here, `‖y‖`) is equal to the length of the hypotenuse (here, `‖x + y‖`) times the sine of the angle adjacent to the opposite side (here, `(o.oangle x (x + y)).sin`).
More concisely: In a 2-dimensional inner product space, the sine of the oriented angle between a vector `x` and its sum with another perpendicular vector `y` equals the norm of `y`.
|
Orientation.oangle_add_right_smul_rotation_pi_div_two
theorem Orientation.oangle_add_right_smul_rotation_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V},
x ≠ 0 → ∀ (r : ℝ), o.oangle x (x + r • (o.rotation ↑(Real.pi / 2)) x) = ↑r.arctan
The theorem `Orientation.oangle_add_right_smul_rotation_pi_div_two` states that for any real vector space `V` of two dimensions with a given orientation `o`, and any non-zero vector `x` in `V`, the angle between `x` and the vector obtained by adding `x` to `r` times the rotation of `x` by `π / 2` (where `r` is a real number), is equal to the arctangent of `r`. In other words, if we rotate `x` by `π / 2` and scale it by `r`, the angle between the original vector and the transformed vector is `arctan(r)`.
More concisely: For any two-dimensional real vector space `V` with orientation `o`, and non-zero vector `x` in `V`, the angle between `x` and `x + r * (π / 2) * ρ(x)` (where `r` is a real number and `ρ(x)` is the counterclockwise rotation of `x` by `π / 2`) is equal to the arctangent of `r`.
|
EuclideanGeometry.cos_oangle_right_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.cos_oangle_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
(EuclideanGeometry.oangle p₂ p₃ p₁).cos = dist p₃ p₂ / dist p₁ p₃
This theorem states that for any three points `p₁`, `p₂`, and `p₃` in a two-dimensional real inner product space (i.e., a space that is like the 2D plane we are familiar with, where "angle" and "distance" have their usual meanings), if the oriented angle from `p₁` through `p₂` to `p₃` (denoted `EuclideanGeometry.oangle p₁ p₂ p₃`) is π/2 radians (which corresponds to a right angle), then the cosine of the oriented angle from `p₂` through `p₃` to `p₁` (denoted `(EuclideanGeometry.oangle p₂ p₃ p₁).cos`) is equal to the ratio of the distance from `p₃` to `p₂` to the distance from `p₁` to `p₃`. This is a statement of the familiar property from Euclidean geometry that in a right-angled triangle, the cosine of an angle is equal to the adjacent side length divided by the hypotenuse length.
More concisely: In a 2D real inner product space, the cosine of the oriented angle between two vectors is equal to the ratio of the length of one vector to the length of the other if and only if the angle is a right angle.
|
Orientation.oangle_sub_right_eq_arcsin_of_oangle_eq_pi_div_two
theorem Orientation.oangle_sub_right_eq_arcsin_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → o.oangle y (y - x) = ↑(‖x‖ / ‖y - x‖).arcsin
This theorem is about an angle in a right-angled triangle in a two-dimensional inner product space over real numbers. It states that if we have a right angle (`pi/2` radians) between two vectors `x` and `y` in this space (given by the orientation `o`), then the angle between `y` and `y - x`, also given by the orientation `o`, is equal to the arcsine of the ratio of the norm of `x` to the norm of `y - x`. This essentially expresses one of the non-right angles of the right-angled triangle in terms of the arcsine function and the lengths of the sides of the triangle.
More concisely: In a two-dimensional real inner product space, given a right angle between vectors `x` and `y` (`||x × y|| = 0`), the angle between `y` and `y - x` is equal to the arcsine of the ratio of `||x||` to `||y - x||`.
|
Orientation.cos_oangle_add_right_of_oangle_eq_pi_div_two
theorem Orientation.cos_oangle_add_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle x (x + y)).cos = ‖x‖ / ‖x + y‖
This theorem is about the cosine of an angle in a right-angled triangle, expressed as a ratio of the lengths of two sides. Specifically, given a two-dimensional vector space `V` over the real numbers, with an associated orientation `o`, and two vectors `x` and `y` in `V`, if the "oriented" angle `o.oangle` between `x` and `y` is equal to π/2 (corresponding to a right angle in geometry), then the cosine of the "oriented" angle between `x` and `x + y` is equal to the ratio of the norm (length) of `x` to the norm of `x + y`. This is a geometric statement that reflects the familiar trigonometric fact from elementary geometry about the cosine of an angle in a right-angled triangle.
More concisely: Given vectors `x` and `y` in a two-dimensional real vector space with orientation `o`, if `o.oangle(x, y) = π/2`, then the cosine of this angle is equal to the ratio of the length of `x` to the length of `x + y`.
|
Orientation.oangle_sub_left_eq_arccos_of_oangle_eq_pi_div_two
theorem Orientation.oangle_sub_left_eq_arccos_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → o.oangle (x - y) x = ↑(‖x‖ / ‖x - y‖).arccos
This theorem is about the angle in a right-angled triangle in a 2-dimensional real inner product space. Specifically, it states that for any normed additive commutative group `V` equipped with an inner product space structure over the real numbers `ℝ`, and having the finite rank 2, given any orientation `o` of `V`, and any two vectors `x` and `y` in `V`, if the orientation angle of `x` and `y` is `π/2` (i.e., they are perpendicular), then the orientation angle of the vectors `x - y` and `x` is equal to the arccosine of the norm of `x` divided by the norm of `x - y`. This essentially expresses one angle of a right-angled triangle using the arccosine function, in terms of the norms of the vectors forming the sides of the triangle.
More concisely: In a 2-dimensional real inner product space with finite rank 2 and given an orientation, the angle between vectors `x` and `y` being perpendicular implies the orientation angle of `x` and `x - y` is equal to the arccosine of `||x|| / ||x - y||`.
|
Orientation.cos_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two
theorem Orientation.cos_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x - y) x).cos * ‖x - y‖ = ‖x‖
This theorem states that in a right-angled triangle in a two-dimensional normed add-commutative group with real inner product space, given that the orientation of the triangle is such that the angle formed by vectors `x` and `y` is equal to π/2 (which corresponds to a 90 degrees angle, making it a right-angled triangle), then the cosine of the angle formed by the vectors `x - y` and `x` multiplied by the norm (length) of the vector `x - y` (which is the hypotenuse of the triangle) is equal to the norm of the vector `x` (which is the adjacent side of the angle formed by the vectors `x - y` and `x`). This theorem essentially represents the geometric relationship in a right-angled triangle captured by the trigonometric identity cos(θ) = adjacent/hypotenuse, but in the context of normed add-commutative groups and inner product spaces.
More concisely: In a right-angled triangle in a two-dimensional normed add-commutative group with real inner product space, the cosine of the angle between vectors `x` and `y`, multiplied by the length of `x - y`, equals the length of `x`.
|
EuclideanGeometry.oangle_right_eq_arccos_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.oangle_right_eq_arccos_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
EuclideanGeometry.oangle p₂ p₃ p₁ = ↑(dist p₃ p₂ / dist p₁ p₃).arccos
This theorem states that, given a right-angled triangle in a Euclidean space of finite dimension 2, if the oriented angle at vertex `p₂` formed by points `p₁`, `p₂`, and `p₃` equals π/2 (indicating a right angle), then the oriented angle at vertex `p₃` formed by points `p₂`, `p₃`, and `p₁` equals the inverse cosine (`arccos`) of the ratio of the distance between points `p₃` and `p₂` to the distance between points `p₁` and `p₃`. This theorem essentially expresses an angle in a right-angled triangle using arccos.
More concisely: In a right-angled triangle in Euclidean space of dimension 2, the angle at vertex `p₃` opposite side `[p₂, p₃]` is equal to `arccos(distance(p₁, p₂) / distance(p₂, p₃))`.
|
Orientation.cos_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two
theorem Orientation.cos_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x + y) y).cos * ‖x + y‖ = ‖y‖
This theorem states that for a real inner product space `V` of finite dimension 2 and any orientation `o` on this space, if the oriented angle `o.oangle` between vectors `x` and `y` is equal to π/2 (i.e., they are orthogonal), then the cosine of the oriented angle between `x + y` and `y` times the norm of `x + y` equals the norm of `y`. This can be seen as a generalization of the Pythagorean theorem to oriented angles in a normed add comm group with an inner product.
More concisely: For any real inner product space of finite dimension 2 with orientation, the cosine of the oriented angle between vectors `x` and `y` being π/2 implies the norm of `y` equals the product of the cosine of the oriented angle between `x+y` and `y`, and the norm of `x+y`.
|
Orientation.tan_oangle_add_right_of_oangle_eq_pi_div_two
theorem Orientation.tan_oangle_add_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle x (x + y)).tan = ‖y‖ / ‖x‖
This theorem, named `Orientation.tan_oangle_add_right_of_oangle_eq_pi_div_two`, states that for any type `V` that is a normed, additive commutative group and has an inner product space over the real numbers with finite dimension equal to 2, and for any orientation `o` of `V`, if the oriented angle `o.oangle` between two vectors `x` and `y` is equal to π/2 (i.e., the vectors are orthogonal), then the tangent of the oriented angle between `x` and the vector sum `x + y` is equal to the ratio of the norm of `y` to the norm of `x`.
This can be seen as a geometric interpretation in 2 dimensions: in a right-angled triangle where `x` and `y` form the right angle, the ratio of the length of the side opposite to the angle formed by `x` and `x + y` (which is the length of `y`) to the length of the adjacent side (which is the length of `x`) is the tangent of that angle.
More concisely: Given a normed, additive commutative group V of finite dimension 2 over the real numbers with an inner product, if vectors x and y are orthogonal with respect to the inner product, then the tangent of the angle between x and x + y is the ratio of the norm of y to the norm of x.
|
Orientation.norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two
theorem Orientation.norm_div_sin_oangle_sub_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → ‖x‖ / (o.oangle y (y - x)).sin = ‖y - x‖
This theorem states that for any normed additively commutative group `V` with an inner product space over the real numbers `ℝ` and a two-dimensional finite rank, given any orientation `o` of `V` and any vectors `x` and `y` in `V`, if the oriented angle `o.oangle x y` equals `π/2`, then the ratio of the norm of `x` to the sine of the oriented angle `o.oangle y (y - x)` is equal to the norm of the vector `y - x`. This theorem is a vector version of the trigonometric relation in a right-angled triangle where a side length divided by the sine of its opposite angle equals the length of the hypotenuse.
More concisely: For any two-dimensional normed additively commutative group `V` over the real numbers `ℝ` with inner product, if the oriented angle between vectors `x` and `y` is a right angle (π/2), then the ratio of the norm of `x` to the sine of the oriented angle between `y` and `(y - x)` is equal to the norm of `y - x`.
|
EuclideanGeometry.dist_div_cos_oangle_right_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.dist_div_cos_oangle_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
dist p₃ p₂ / (EuclideanGeometry.oangle p₂ p₃ p₁).cos = dist p₁ p₃
This theorem states that in a right-angled triangle (in a two-dimensional real inner-product space, or Euclidean space), if the angle at a point `p₂` between line segments `p₂p₁` and `p₂p₃` is π/2 (which indicates a right angle), then the length of the side `p₃p₂` divided by the cosine of the angle at `p₃` between `p₃p₂` and `p₃p₁` is equal to the length of the hypotenuse `p₁p₃`.
More concisely: In a right-angled triangle in a two-dimensional Euclidean space, the length of the side opposite the right angle divided by the cosine of the angle next to the right angle is equal to the length of the hypotenuse.
|
EuclideanGeometry.sin_oangle_right_mul_dist_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.sin_oangle_right_mul_dist_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
(EuclideanGeometry.oangle p₂ p₃ p₁).sin * dist p₁ p₃ = dist p₁ p₂
The theorem `EuclideanGeometry.sin_oangle_right_mul_dist_of_oangle_eq_pi_div_two` states that in a right-angled triangle, where the given angle is equal to π/2, the length of the opposite side is equal to the length of the hypotenuse multiplied by the sine of another angle. More specifically, for a metric space `P`, with `V` as its associated normed add commutative group, under the conditions that `V` is a real inner product space, a normed add torsor, and an oriented 2-dimensional real module, if `p₁`, `p₂`, and `p₃` are points in `P` such that the oriented angle from `p₁` to `p₂` to `p₃` is π/2, then the sine of the oriented angle from `p₂` to `p₃` to `p₁` times the distance from `p₁` to `p₃` equals the distance from `p₁` to `p₂`.
More concisely: In a right-angled triangle with an angle of π/2, the length of the opposite side is equal to the hypotenuse multiplied by the sine of the adjacent angle.
|
EuclideanGeometry.tan_oangle_right_mul_dist_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.tan_oangle_right_mul_dist_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
(EuclideanGeometry.oangle p₂ p₃ p₁).tan * dist p₃ p₂ = dist p₁ p₂
This theorem, from Euclidean Geometry, states that given a right-angled triangle in a two-dimensional inner product space, if the angle at the second point (p₂) is π/2 (a right angle), then the tangent of the angle at the third point (p₃) multiplied by the distance between the second and third points (p₂ and p₃) equals the distance between the first and second points (p₁ and p₂). Here, distances and angles are calculated in the normed add torsor over the normed add commutative group V. The theorem essentially formalizes in Lean 4 one of the key relationships in a right-angled triangle, which is traditionally known as "the opposite is equal to the adjacent times the tangent of the angle".
More concisely: In a right-angled triangle in a two-dimensional inner product space, the tangent of the angle between the second and third points multiplied by the distance between the second and third points equals the distance between the first and second points.
|
Orientation.tan_oangle_add_right_smul_rotation_pi_div_two
theorem Orientation.tan_oangle_add_right_smul_rotation_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V},
x ≠ 0 → ∀ (r : ℝ), (o.oangle x (x + r • (o.rotation ↑(Real.pi / 2)) x)).tan = r
This theorem states that in a right-angled triangle, the tangent of an angle is equal to the ratio of the lengths of the side opposite the angle to the side adjacent to the angle. More precisely, if we have a 2-dimensional oriented normed commutative group with an inner product space over the real numbers, for any non-zero vector `x` in the group, and any real number `r`, if we rotate `x` by `π/2` radians (90 degrees), scale the rotated vector by `r` and add the result back to `x`, the tangent of the oriented angle from `x` to the resulting vector is exactly `r`. This is analogous to the geometric concept that in a right triangle, the tangent of an angle is the ratio of the length of the side opposite the angle (the "opposite") to the length of the side adjacent to the angle (the "adjacent"), except here our "triangle" is formed by `x`, the zero vector, and `x + r • (o.rotation ↑(Real.pi / 2)) x`.
More concisely: In a 2-dimensional oriented normed commutative group with an inner product space over the real numbers, the tangent of the angle between any non-zero vector and the vector rotated 90 degrees counterclockwise and scaled by a real number is equal to the scaling factor.
|
EuclideanGeometry.sin_oangle_left_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.sin_oangle_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
(EuclideanGeometry.oangle p₃ p₁ p₂).sin = dist p₃ p₂ / dist p₁ p₃
This theorem states that in a two-dimensional Euclidean geometry, for any three points $p_1$, $p_2$, and $p_3$, if the oriented angle $\angle p_1p_2p_3$ is $\pi/2$ (or 90 degrees), then the sine of the oriented angle $\angle p_3p_1p_2$ is equal to the ratio of the distance between points $p_3$ and $p_2$ to the distance between points $p_1$ and $p_3$. In other words, it describes the relationship of the sine of an angle in a right-angled triangle to the ratio of the lengths of the sides of the triangle.
This theorem is based in the context of a real inner product space with a two-dimensional normed additively commutative group and a metric space, and also assumes that the two-dimensional space is oriented. It makes use of the concepts of the rank of a module, π (pi), and sine, as well as distances and angles in Euclidean geometry.
More concisely: In two-dimensional Euclidean geometry, the sine of the angle between two sides of a right triangle is equal to the ratio of the length of the hypotenuse to the length of the adjacent side.
|
Orientation.tan_oangle_add_left_of_oangle_eq_pi_div_two
theorem Orientation.tan_oangle_add_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x + y) y).tan = ‖x‖ / ‖y‖
The theorem `Orientation.tan_oangle_add_left_of_oangle_eq_pi_div_two` states that in the context of a 2-dimensional real inner product space with a given orientation, if the orientation angle between two vectors `x` and `y` is `π/2` (which is 90 degrees and indicates that the vectors are orthogonal), then the tangent of the orientation angle between the vector `x + y` and the vector `y` is equal to the ratio of the norm of `x` to the norm of `y`. This is analogous to the geometric concept in right-angled triangles where the tangent of an angle is the ratio of the lengths of the opposite side to the adjacent side.
More concisely: In a 2-dimensional real inner product space with a given orientation, the tangent of the orientation angle between vectors `x` and `y` is equal to the norm of `x` divided by the norm of `y` when the angle between them is `π/2`.
|
Orientation.norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two
theorem Orientation.norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → ‖y‖ / (o.oangle x (x + y)).tan = ‖x‖
This theorem states that in a right-angled triangle formed within a real 2-dimensional inner product space, if the oriented angle between vectors `x` and `y` equals π/2 (i.e., the vectors are orthogonal), then the length of vector `y` divided by the tangent of the oriented angle between `x` and the vector sum of `x` and `y` equals the length of vector `x`. In other words, this theorem relates the lengths of the vectors and the oriented angles they form to each other in a way that mirrors the geometric properties of a right-angled triangle. The theorem assumes that the space has an orientation.
More concisely: In a real 2-dimensional inner product space with orientation, the ratio of the length of vector `y` to the tangent of the oriented angle between vectors `x` and `(x ⊕ y)` equals the length of vector `x`, where `x` and `y` are orthogonal.
|
Orientation.tan_oangle_add_left_smul_rotation_pi_div_two
theorem Orientation.tan_oangle_add_left_smul_rotation_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V},
x ≠ 0 →
∀ (r : ℝ), (o.oangle (x + r • (o.rotation ↑(Real.pi / 2)) x) (r • (o.rotation ↑(Real.pi / 2)) x)).tan = r⁻¹
This theorem states that in the context of a real inner product space `V` of finite rank 2, for any non-zero vector `x` and real number `r` in this space, and given an orientation `o` of the space, the tangent of the angle formed by the sum vector `x + r • (o.rotation ↑(Real.pi / 2)) x` and the rotated vector `r • (o.rotation ↑(Real.pi / 2)) x`, where `o.rotation ↑(Real.pi / 2)` represents a rotation by pi/2 radians, is equal to the reciprocal of `r`. This is akin to the trigonometric concept where the tangent of an angle in a right-angled triangle is the ratio of the opposite side to the adjacent side. In this case, `r` is essentially playing the role of the adjacent side and the other vector forms the opposite side.
More concisely: In a real inner product space of finite rank 2, the tangent of the angle between a vector `x` and the rotated vector `r * (o.rotation (π/2) x)` is equal to the reciprocal of `r`, where `o` is an orientation and `*` denotes the scalar multiplication.
|
Orientation.tan_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two
theorem Orientation.tan_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x - y) x).tan * ‖x‖ = ‖y‖
This theorem states that for a normed add commutative group `V` with an inner product space over the real numbers, which has a two-dimensional finite rank, and an orientation `o`, if the oriented angle `o.oangle` between vectors `x` and `y` is equal to π/2 (i.e., the vectors are perpendicular), then the tangent of the oriented angle between `x - y` and `x` multiplied by the norm of `x` equals the norm of `y`. This result reflects the geometric concept in a right-angled triangle that the length of the side opposite the right angle (norm of `y`) is equal to the length of the adjacent side (norm of `x`) times the tangent of the angle between them.
More concisely: For a two-dimensional real inner product space `V` with orientation `o`, if vectors `x` and `y` are perpendicular (have angle `o.oangle = π/2), then the norm of `x - y` times the tangent of `π/4` is equal to the norm of `y`.
|
EuclideanGeometry.dist_div_tan_oangle_left_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.dist_div_tan_oangle_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
dist p₃ p₂ / (EuclideanGeometry.oangle p₃ p₁ p₂).tan = dist p₁ p₂
This theorem states that in a right-angled triangle, the length of a side (the distance between points p₃ and p₂) divided by the tangent of the angle opposite to that side (the angle at p₃ formed by points p₃, p₁, and p₂) equals the length of the adjacent side (the distance between points p₁ and p₂). This is under the conditions that we are working in a 2-dimensional real inner product space, which has a specified orientation.
More concisely: In a right-angled triangle in a 2-dimensional real inner product space with a specified orientation, the ratio of the length of the hypotenuse to the tangent of the angle opposite it is equal to the length of the adjacent side.
|
Orientation.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two
theorem Orientation.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → o.oangle x (x + y) = ↑(‖y‖ / ‖x‖).arctan
This theorem states that for a right-angled triangle in an oriented two-dimensional real inner product space, if the orientation angle between vectors `x` and `y` is π/2 (or 90 degrees), then the orientation angle between vectors `x` and the vector sum of `x` and `y` is equal to the arctangent of the ratio of the norm of `y` to the norm of `x`. This essentially relates the orientation angle to the arctangent function in the context of right-angled triangles, reflecting the geometric interpretation of the arctangent function as the angle formed with the positive x-axis by a line passing through the origin and a point `(1, t)` for `t = ‖y‖ / ‖x‖`, which is a common setup in trigonometry.
More concisely: For a right-angled triangle in an oriented two-dimensional real inner product space, the orientation angle between a vector `x` and the vector sum of `x` and `y` is equal to the arctangent of the norm ratio of `y` to `x`.
|
Orientation.sin_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two
theorem Orientation.sin_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x - y) x).sin * ‖x - y‖ = ‖y‖
This theorem states that for a space `V` of real inner products, which is a normed add commutative group and has a finite rank of 2, and given an orientation `o`, for any vectors `x` and `y` in that space, if the oriented angle `o.oangle` between `x` and `y` is equal to right angle (π/2 in radians), then the sine of the oriented angle between the vector difference `x - y` and `x`, multiplied by the norm of this difference `‖x - y‖`, will be equal to the norm of vector `y` `‖y‖`. This is essentially a variation of the geometric concept where the length of the side opposite a right angle in a right-angled triangle is obtained by multiplying the hypotenuse length by the sine of the angle opposite to the side.
More concisely: For a real inner product space of finite rank 2 with orientation and vectors x, y, if the oriented angle between x and y is a right angle, then the product of the sine of that angle and the norm of x - y is equal to the norm of y.
|
Orientation.norm_div_tan_oangle_sub_left_of_oangle_eq_pi_div_two
theorem Orientation.norm_div_tan_oangle_sub_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → ‖y‖ / (o.oangle (x - y) x).tan = ‖x‖
This theorem states that in a right-angled triangle in a two-dimensional inner product space over the real numbers, if one angle is pi/2 (which corresponds to a right angle), then the ratio of the length (or norm) of the side opposite this angle to the tangent of the angle formed by subtracting the vectors of the two sides adjacent to the right angle, equals the length (or norm) of the side adjacent to the right angle. This theorem is a generalized version of a familiar trigonometric identity in the context of vector spaces and it utilizes concepts such as orientations and angles in those spaces.
More concisely: In a right-angled triangle in a 2-dimensional real inner product space, the ratio of the norm of the side opposite the right angle to the norm of the difference of the norms of the other two sides is equal to one.
|
Orientation.cos_oangle_add_left_of_oangle_eq_pi_div_two
theorem Orientation.cos_oangle_add_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x + y) y).cos = ‖y‖ / ‖x + y‖
This theorem, `Orientation.cos_oangle_add_left_of_oangle_eq_pi_div_two`, states that in a 2-dimensional real inner product space, if the oriented angle between two vectors `x` and `y` is π/2 (i.e., the two vectors are orthogonal), then the cosine of the oriented angle between `x + y` and `y` is the ratio of the norm of `y` to the norm of `x + y`. This is a geometrical statement akin to expressing the cosine of an angle in a right-angled triangle as a ratio of sides.
More concisely: In a 2-dimensional real inner product space, if vectors `x` and `y` are orthogonal, then the cosine of the oriented angle between `x + y` and `y` is the ratio of the norm of `y` to the norm of `x + y`.
|
EuclideanGeometry.dist_div_cos_oangle_left_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.dist_div_cos_oangle_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
dist p₁ p₂ / (EuclideanGeometry.oangle p₃ p₁ p₂).cos = dist p₁ p₃
This theorem, from the field of Euclidean geometry, states that for any points `p₁`, `p₂`, and `p₃` in a two-dimensional real inner product space with a given orientation, if the oriented angle `p₁ p₂ p₃` is equal to π/2 (which corresponds to a right angle), then the ratio of the distance from `p₁` to `p₂` to the cosine of the oriented angle `p₃ p₁ p₂` is equal to the distance from `p₁` to `p₃`. This corresponds to the geometric property of a right-angled triangle where the length of a side adjacent to an angle, divided by the cosine of that angle, equals the length of the hypotenuse.
More concisely: In a two-dimensional real inner product space, the ratio of the distance between points `p₁` and `p₂` to the cosine of the oriented angle between `p₂` and `p₁`, is equal to the distance between `p₁` and `p₃` if and only if the angle `p₁ p₂ p₃` is a right angle (π/2 radians).
|
EuclideanGeometry.dist_div_sin_oangle_left_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.dist_div_sin_oangle_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
dist p₃ p₂ / (EuclideanGeometry.oangle p₃ p₁ p₂).sin = dist p₁ p₃
This theorem states that for any three points `p₁`, `p₂`, and `p₃` in a two-dimensional Euclidean space over a real vector space, if the oriented angle at `p₂` formed by the vectors from `p₂` to `p₁` and from `p₂` to `p₃` equals π/2 (a right angle), then the distance from `p₃` to `p₂` divided by the sine of the oriented angle at `p₃` formed by the vectors from `p₃` to `p₁` and from `p₃` to `p₂` equals the distance from `p₁` to `p₃`. This is a formalization of a special case of the Law of Sines from trigonometry, which in this case becomes the geometric relationship in a right-angled triangle where a side length divided by the sine of the opposite angle equals the length of the hypotenuse.
More concisely: In a two-dimensional Euclidean space, if the oriented angle between vectors from point `p₂` to `p₁` and from `p₂` to `p₃` is a right angle (π/2), then the ratio of the distance from `p₂` to `p₃` to the sine of the angle between vectors from `p₃` to `p₁` and from `p₃` to `p₂` equals the distance from `p₁` to `p₃`.
|
Orientation.sin_oangle_sub_right_of_oangle_eq_pi_div_two
theorem Orientation.sin_oangle_sub_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle y (y - x)).sin = ‖x‖ / ‖y - x‖
This theorem, `Orientation.sin_oangle_sub_right_of_oangle_eq_pi_div_two`, states that for any real inner product space `V` of finite rank 2, any orientation `o` of `V`, and any two vectors `x` and `y` in `V`, if the oriented angle `o.oangle` between `x` and `y` equals π/2 (which means that `x` and `y` are orthogonal in the sense of the inner product), then the sine of the oriented angle between `y` and `y - x` equals the norm of `x` divided by the norm of `y - x`. This is a geometric statement about right-angled triangles formed by vectors in the inner product space: it relates the sine of an angle in such a triangle to ratios of side lengths.
More concisely: For any finite rank 2 real inner product space V, orientation o, and vectors x, y in V with o.oangle(x, y) = π/2, the sine of o.oangle(y, y - x) equals the norm of x divided by the norm of y - x.
|
Orientation.norm_div_cos_oangle_sub_left_of_oangle_eq_pi_div_two
theorem Orientation.norm_div_cos_oangle_sub_left_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → ‖x‖ / (o.oangle (x - y) x).cos = ‖x - y‖
This theorem states that for a normed additive 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 vectors `x` and `y` in `V`, if the oriented angle `o.oangle` between `x` and `y` equals π/2 (suggesting a right angle), then the ratio of the norm of `x` to the cosine of the oriented angle between `x - y` and `x` equals the norm of `x - y`. This resembles the geometric property of a right-angled triangle that a side length divided by the cosine of the adjacent angle equals the hypotenuse.
More concisely: For a finite rank 2 real inner product space `V` with orientation `o`, if the oriented angle between vectors `x` and `y` is π/2, then the ratio of `x`'s norm to the cosine of this angle between `x-y` and `x` equals the norm of `x-y`.
|
EuclideanGeometry.cos_oangle_left_mul_dist_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.cos_oangle_left_mul_dist_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
(EuclideanGeometry.oangle p₃ p₁ p₂).cos * dist p₁ p₃ = dist p₁ p₂
This theorem is a formulation of a basic trigonometric principle in the context of Euclidean geometry. Specifically, it states that for a right-angled triangle defined by points `p₁`, `p₂`, and `p₃` in a 2-dimensional Euclidean space with an inner product over real numbers, if the oriented angle `oangle` at `p₂` (formed by the line segments from `p₂` to `p₁` and from `p₂` to `p₃`) is equal to π/2 (i.e., a right angle), then the product of the cosine of the oriented angle at `p₁` (formed by the line segments from `p₁` to `p₃` and from `p₁` to `p₂`) and the distance between `p₁` and `p₃` will equal the distance between `p₁` and `p₂`. This is analogous to the trigonometric identity that in a right-angled triangle, the length of the adjacent side is equal to the hypotenuse times the cosine of the angle.
More concisely: In a right-angled triangle in a 2-dimensional Euclidean space with an inner product over real numbers, the cosine of the angle between the legs multiplied by the length of the hypotenuse is equal to the length of the adjacent leg.
|
EuclideanGeometry.tan_oangle_left_mul_dist_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.tan_oangle_left_mul_dist_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) →
(EuclideanGeometry.oangle p₃ p₁ p₂).tan * dist p₁ p₂ = dist p₃ p₂
This theorem states that in a right-angled triangle, the tangent of one of the angles, when multiplied by the length of the adjacent side, gives the length of the opposite side. More specifically, given a Euclidean space `V` of finite dimension 2 with the standard orientation, and given three points `p₁`, `p₂`, and `p₃` in a metric space `P` associated with `V` such that the angle at `p₂` (denoted as `EuclideanGeometry.oangle p₁ p₂ p₃`) is π/2 radians (i.e., a right angle), the product of the tangent of the angle at `p₁` (denoted as `EuclideanGeometry.oangle p₃ p₁ p₂`.tan) and the distance between `p₁` and `p₂` (denoted as `dist p₁ p₂`) equals the distance between `p₃` and `p₂` (denoted as `dist p₃ p₂`). This is a formal statement of a well-known trigonometric identity related to right-angled triangles.
More concisely: In a right-angled triangle, the tangent of the angle opposite the side of length `dist(p₁, p₂)` times the length of the adjacent side `dist(p₂, p₁)` equals the length of the hypotenuse `dist(p₃, p₂)`.
|
Orientation.oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two
theorem Orientation.oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → o.oangle y (y - x) = ↑(‖x‖ / ‖y‖).arctan
This theorem states that for a right-angled triangle in a 2-dimensional inner product space over the real numbers, given the orientation of the space and two vectors `x` and `y` such that the angle between `x` and `y` is π/2 (right angle), the angle between `y` and `y - x` (i.e., the angle that `y` makes with the vector pointing from `x` to `y`) is equal to the arctangent of the ratio of the norms (lengths) of `x` and `y`. This result connects the geometry of right-angled triangles with trigonometric functions and vector operations.
More concisely: In a 2-dimensional real inner product space, the angle between vectors `x` and `y` forming a right angle is equal to the arctangent of the quotient of the norms of `x` and `y`.
|
Orientation.tan_oangle_sub_right_of_oangle_eq_pi_div_two
theorem Orientation.tan_oangle_sub_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x y : V},
o.oangle x y = ↑(Real.pi / 2) → (o.oangle y (y - x)).tan = ‖x‖ / ‖y‖
This theorem states that in the context of a real inner product space `V` of finite dimension 2 and an orientation `o` of `V`, given two vectors `x` and `y` such that the oriented angle `o.oangle` between `x` and `y` equals π/2, the tangent of the oriented angle between `y` and the vector difference `y - x` equals the ratio of the norm of `x` over the norm of `y`. In simple terms, it's a rule of trigonometry stating that in a right-angled triangle formed by `x`, `y` and `y - x`, the tangent of the angle at `y` equals the ratio of the lengths of the side opposite to the angle (corresponding to `x`) and the side adjacent to the angle (corresponding to `y`).
More concisely: In a real inner product space of finite dimension 2 with given orientation, the tangent of the oriented angle between a vector and the vector difference of another vector and it, forming a right angle, equals the ratio of the norms of the first vector and the second vector.
|