InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero
theorem InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x ≠ 0 → InnerProductGeometry.angle x (x + y) = (‖y‖ / ‖x‖).arctan
This theorem states that in a right-angled triangle, the angle can be expressed using the `arctan` function, given that the inner product of two vectors `x` and `y` is zero and vector `x` is not zero. More formally, for any normed add commutative group `V` that is also an inner product space over the real numbers, and any two vectors `x` and `y` in `V`, if the inner product of `x` and `y` is zero (indicating that they are orthogonal) and `x` is not the zero vector, then the angle between `x` and the vector obtained by adding `x` and `y` is equal to the `arctan` of the ratio of the norms of `y` and `x`. This corresponds to the trigonometric concept that in a right-angled triangle, the tangent of an angle is the ratio of the lengths of the opposite side to the adjacent side.
More concisely: In a right-angled triangle with orthogonal vectors x and y, the angle between x and y is equal to the arctangent of the ratio of the norms of y and x.
|
EuclideanGeometry.angle_eq_arctan_of_angle_eq_pi_div_two
theorem EuclideanGeometry.angle_eq_arctan_of_angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
p₃ ≠ p₂ → EuclideanGeometry.angle p₂ p₃ p₁ = (dist p₁ p₂ / dist p₃ p₂).arctan
This theorem is about an angle of a right-angled triangle in Euclidean geometry. Specifically, it states that if the angle at `p2` between line segments to `p1` and `p3` is equal to π/2 (making it a right angle), and provided `p3` is not equal to `p2`, then the angle at `p3` between line segments to `p2` and `p1` is equal to the arctan of the ratio of the distances between `p1` and `p2` and between `p3` and `p2`. In essence, this theorem demonstrates a way to express one of the angles in a right-angled triangle using the arctan function and the lengths of the triangle's sides.
More concisely: In a right-angled triangle with sides of lengths `lp1p2` and `lp2p3` (where `p1`, `p2`, and `p3` are the corresponding points), if the angle at `p2` is a right angle, then the angle at `p3` is equal to arctan(lp1p2 / lp2p3).
|
EuclideanGeometry.angle_lt_pi_div_two_of_angle_eq_pi_div_two
theorem EuclideanGeometry.angle_lt_pi_div_two_of_angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 → p₃ ≠ p₂ → EuclideanGeometry.angle p₂ p₃ p₁ < Real.pi / 2
This theorem states that in a non-degenerate right-angled triangle, any angle is less than `π / 2` (or 90 degrees) if it is not the right angle itself. The angle is measured at a point `p₂` between the line segments to points `p₁` and `p₃`. If the angle between `p₁`, `p₂`, and `p₃` is `π / 2` (i.e., a right angle) and `p₃` is not equal to `p₂`, then the angle between `p₂`, `p₃` and `p₁` is less than `π / 2`. Here, `V` represents a normed add commutative group, `P` a metric space, and `V` and `P` are related by a normed add torsor, which allows us to perform vector space operations on the points in `P`.
More concisely: In a non-degenerate right-angled triangle, any angle other than the right angle is less than π/2 (90 degrees).
|
InnerProductGeometry.angle_sub_eq_arcsin_of_inner_eq_zero
theorem InnerProductGeometry.angle_sub_eq_arcsin_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x ≠ 0 ∨ y ≠ 0 → InnerProductGeometry.angle x (x - y) = (‖y‖ / ‖x - y‖).arcsin
The theorem `InnerProductGeometry.angle_sub_eq_arcsin_of_inner_eq_zero` states that in a right-angled triangle, the angle between vectors `x` and `x - y` is equal to the arcsine of the norm of vector `y` divided by the norm of the vector `x - y`. This is under conditions where the inner product of the vectors `x` and `y` is zero (indicating that the vectors are orthogonal or at least one of them is zero), and at least one of the vectors `x` and `y` isn't zero.
More concisely: In a right-angled triangle representing vectors `x` and `y` with inner product equal to zero and neither being the zero vector, the angle between them equals the arcsine of the magnitude of `y` divided by the magnitude of `x - y`.
|
InnerProductGeometry.angle_sub_le_pi_div_two_of_inner_eq_zero
theorem InnerProductGeometry.angle_sub_le_pi_div_two_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → InnerProductGeometry.angle x (x - y) ≤ Real.pi / 2
This theorem states that in the context of a real inner product space, if the inner product of two vectors 'x' and 'y' is zero (⟪x, y⟫_ℝ = 0, which usually means 'x' and 'y' are orthogonal or at least one of them is a zero vector), then the undirected angle between vector 'x' and the vector resulting from the subtraction of 'y' from 'x' (x - y) is at most π / 2. In other words, any angle in a right-angled triangle, formed from these vectors, does not exceed 90 degrees.
More concisely: In a real inner product space, if the inner product of two vectors is zero, then the angle between them is at most 90 degrees.
|
EuclideanGeometry.angle_pos_of_angle_eq_pi_div_two
theorem EuclideanGeometry.angle_pos_of_angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 → p₁ ≠ p₂ ∨ p₃ = p₂ → 0 < EuclideanGeometry.angle p₂ p₃ p₁
The theorem `EuclideanGeometry.angle_pos_of_angle_eq_pi_div_two` states that for any non-degenerate right-angled triangle (a triangle in which no two points coincide), if the angle at a point is π/2 (or, equivalently, 90 degrees), then the other two angles are positive. This is stated more formally as: given any three points `p₁`, `p₂`, and `p₃`, if the angle at `p₂` between `p₁` and `p₃` is π/2 and `p₁` is not the same point as `p₂` or `p₃` is the same point as `p₂`, then the angle at `p₃` between `p₂` and `p₁` is positive.
More concisely: In a non-degenerate right-angled triangle, the angle opposite the right angle is positive.
|
InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero
theorem InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → (InnerProductGeometry.angle x (x + y)).cos * ‖x + y‖ = ‖x‖
This theorem states that for any real inner product space, if the inner product of two vectors `x` and `y` is zero, then the cosine of the angle between `x` and `x + y` multiplied by the norm of `x + y` equals the norm of `x`. In terms of geometry, this corresponds to the situation where `x` and `y` are perpendicular (since their inner product is zero), and the theorem then gives a relationship involving the angle between `x` and `x + y`, which forms a right-angled triangle with `x` and `y`.
More concisely: For any real inner product space, the cosine of the angle between two vectors `x` and `y` equals the norm of `x` divided by the norm of `x + y` if and only if `x` and `y` are orthogonal (have inner product equal to zero).
|
InnerProductGeometry.sin_angle_sub_of_inner_eq_zero
theorem InnerProductGeometry.sin_angle_sub_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x ≠ 0 ∨ y ≠ 0 → (InnerProductGeometry.angle x (x - y)).sin = ‖y‖ / ‖x - y‖
This theorem, named `InnerProductGeometry.sin_angle_sub_of_inner_eq_zero`, asserts that in the context of an InnerProductSpace over the real number ℝ with a NormedAddCommGroup V, if the inner product of two vectors 'x' and 'y' equals zero (⟪x, y⟫_ℝ = 0) and at least one of the vectors is non-zero (x ≠ 0 ∨ y ≠ 0), then the sine of the angle between vector 'x' and the difference of vectors 'x' and 'y' (InnerProductGeometry.angle x (x - y)) is obtained as the ratio of the norm of vector 'y' to the norm of the difference of vectors 'x' and 'y' (‖y‖ / ‖x - y‖). In this theorem, the angle is understood as the undirected angle between two vectors, which equals π/2 if either vector is zero.
More concisely: If the inner product of two non-zero vectors in a real inner product space is zero, then the sine of the angle between one vector and the difference of the two vectors is equal to the norm of the other vector divided by the norm of their difference.
|
EuclideanGeometry.dist_div_sin_angle_of_angle_eq_pi_div_two
theorem EuclideanGeometry.dist_div_sin_angle_of_angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
p₁ ≠ p₂ ∨ p₃ = p₂ → dist p₁ p₂ / (EuclideanGeometry.angle p₂ p₃ p₁).sin = dist p₁ p₃
This theorem states that in a right-angled triangle, if the angle at `p₂` between lines `p₁p₂` and `p₂p₃` is equal to π/2 (i.e., it's a right angle), then the ratio of the distance from `p₁` to `p₂` to the sine of the angle at `p₃` between lines `p₂p₃` and `p₃p₁` is equal to the distance from `p₁` to `p₃`. In simpler terms, this theorem is a precise mathematical formulation of a property of right triangles, specifically a variation of the Law of Sines: the length of a side of a right triangle divided by the sine of the opposite angle equals the length of the hypotenuse.
More concisely: In a right-angled triangle, the ratio of the length of the side adjacent to the right angle to the sine of the angle opposite the right angle is equal to the length of the hypotenuse.
|
InnerProductGeometry.sin_angle_sub_mul_norm_of_inner_eq_zero
theorem InnerProductGeometry.sin_angle_sub_mul_norm_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → (InnerProductGeometry.angle x (x - y)).sin * ‖x - y‖ = ‖y‖
This theorem states that in the context of an inner product space over the real numbers, for any two vectors `x` and `y`, if their inner product is zero, then the sine of the angle between vector `x` and the vector difference `x - y`, multiplied by the norm (magnitude) of the vector difference `x - y`, equals the norm of vector `y`. This is analogues to the geometrical fact in a right-angled triangle that the sine of an angle times the length of the hypotenuse equals the length of the opposite side.
More concisely: In an inner product space over the real numbers, the sine of the angle between vectors `x` and `x-y` times the norm of `x-y` equals the norm of `y`, given that `x · y` (the inner product of `x` and `y`) is zero.
|
InnerProductGeometry.sin_angle_add_of_inner_eq_zero
theorem InnerProductGeometry.sin_angle_add_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x ≠ 0 ∨ y ≠ 0 → (InnerProductGeometry.angle x (x + y)).sin = ‖y‖ / ‖x + y‖
This theorem describes the sine of the angle in a right-angled triangle formed by two vectors in an inner product space over the real numbers. More specifically, if the inner product of vectors `x` and `y` is zero and at least one of them is non-zero, then the sine of the angle between `x` and `x + y` is equal to the ratio of the norm of `y` to the norm of `x + y`. This corresponds to the geometric concept of the sine of an angle in a right triangle being the ratio of the length of the opposite side to the hypotenuse.
More concisely: If vectors `x` and `y` in an inner product space over the real numbers have zero inner product and `x ≠ 0`, then the sine of the angle between `x` and `x + y` equals the ratio of the norm of `y` to the norm of `x + y`.
|
EuclideanGeometry.cos_angle_mul_dist_of_angle_eq_pi_div_two
theorem EuclideanGeometry.cos_angle_mul_dist_of_angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
(EuclideanGeometry.angle p₂ p₃ p₁).cos * dist p₁ p₃ = dist p₃ p₂
This theorem states that in a right-angled triangle, the cosine of an angle multiplied by the length of the hypotenuse is equal to the length of the adjacent side. In the context of Euclidean geometry, given three points p₁, p₂, and p₃ with the angle at p₂ being π/2 radians (which forms a right angle), the cosine of the angle at p₃ multiplied by the distance between p₁ and p₃ (which forms the hypotenuse) equals the distance between p₃ and p₂ (which is the side adjacent to the angle at p₃).
More concisely: In a right-angled triangle, the cosine of the angle between the hypotenuse and the adjacent side is equal.
|
InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two
theorem InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ InnerProductGeometry.angle x y = Real.pi / 2
This theorem is a form of the Pythagorean theorem for vectors in an inner product space. It states that for any two vectors `x` and `y` in a normed add commutative group that also forms a real inner product space, the square of the norm of the sum of `x` and `y` equals the sum of the squares of the norms of `x` and `y` if and only if the undirected angle between `x` and `y` is π/2 (or equivalently, the vectors are orthogonal). In other words, it generalizes the Pythagorean theorem to vectors, which can measure not just lengths (norms), but also the angle between two vectors.
More concisely: For vectors x and y in a real inner product space, the square of the norm of their sum equals the sum of the squares of their norms if and only if they are orthogonal (have an angle of π/2 between them).
|
EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two
theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_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] (p1 p2 p3 : P),
dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 ↔
EuclideanGeometry.angle p1 p2 p3 = Real.pi / 2
This is a version of the Pythagorean theorem, which states that in a Euclidean geometry with points P1, P2, and P3, the square of the distance between P1 and P3 is equal to the sum of the square of the distance between P1 and P2 and the square of the distance between P3 and P2 if and only if the undirected angle at P2 between the line segments to P1 and P3 is π/2. In other words, it gives a condition for when a triangle formed by three points is a right-angled triangle at P2.
More concisely: In a Euclidean geometry, the square of the length of the hypotenuse is equal to the sum of the squares of the lengths of the other two sides of a right-angled triangle.
|
InnerProductGeometry.angle_add_le_pi_div_two_of_inner_eq_zero
theorem InnerProductGeometry.angle_add_le_pi_div_two_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → InnerProductGeometry.angle x (x + y) ≤ Real.pi / 2
The theorem states that in the context of an inner product space over the real numbers, if two vectors `x` and `y` are orthogonal (i.e., their inner product is zero), then the unoriented angle between vector `x` and the sum of vectors `x` and `y` is less than or equal to `π / 2`. This is analogous to the geometric fact that any angle in a right-angle triangle is at most `π / 2` radians, or 90 degrees.
More concisely: In an inner product space over the real numbers, if vectors `x` and `y` are orthogonal then the unoriented angle between `x` and `x + y` is less than or equal to π/2.
|
InnerProductGeometry.cos_angle_sub_mul_norm_of_inner_eq_zero
theorem InnerProductGeometry.cos_angle_sub_mul_norm_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → (InnerProductGeometry.angle x (x - y)).cos * ‖x - y‖ = ‖x‖
This theorem states that for any inner product space over the real numbers, given two vectors `x` and `y` such that their inner product is zero, the cosine of the angle between `x` and the vector resulting from subtracting `y` from `x`, multiplied by the norm of this resultant vector, equals the norm of `x`. This is a version of the trigonometric principle that in a right-angled triangle, the cosine of an angle multiplied by the length of the hypotenuse equals the length of the adjacent side, applicable to the context of vector spaces with an inner product.
More concisely: For any inner product space over the real numbers, the cosine of the angle between vectors `x` and `x-y` is equal to the norm of `x` if `x` and `y` have zero inner product.
|
InnerProductGeometry.norm_div_sin_angle_sub_of_inner_eq_zero
theorem InnerProductGeometry.norm_div_sin_angle_sub_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x = 0 ∨ y ≠ 0 → ‖y‖ / (InnerProductGeometry.angle x (x - y)).sin = ‖x - y‖
This theorem in the context of inner product geometry states that for any vectors `x` and `y` in a real inner product space where their inner product equals to zero, with the condition that `x` is either the zero vector or `y` is not the zero vector. The norm (or length) of vector `y` divided by the sine of the angle between vectors `x` and `(x - y)` is equal to the norm of the vector `x - y`. This theorem is a vector version of the trigonometric identity which relates the sides and angles of a right-angled triangle.
More concisely: For vectors `x` and `y` in a real inner product space with `∥x∥ ≠ 0`, if `∥x∥ * ∣sin(θ)∣ = ∥y∥` where `θ` is the angle between `x` and `(x - y)`, then `x` is the zero vector or `y` is the opposite side of a right angle to `x`. In this case, `∥x - y∥ = ∥y∥`.
|
EuclideanGeometry.angle_eq_arcsin_of_angle_eq_pi_div_two
theorem EuclideanGeometry.angle_eq_arcsin_of_angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
p₁ ≠ p₂ ∨ p₃ ≠ p₂ → EuclideanGeometry.angle p₂ p₃ p₁ = (dist p₁ p₂ / dist p₁ p₃).arcsin
This theorem states that in a right-angled triangle, if the angle at point `p₂` between line segments to `p₁` and `p₃` is π/2 (90 degrees), given that `p₁` is not equal to `p₂` or `p₃` is not equal to `p₂`, then the angle at `p₂` between line segments to `p₃` and `p₁` can be expressed using the inverse sine (arcsin) of the ratio of the distance between `p₁` and `p₂` to the distance between `p₁` and `p₃`.
More concisely: In a right-angled triangle, the angle at a vertex opposite to the side with length the ratio of the leg to hypotenuse being `x`, is equal to arcsin(x).
|
InnerProductGeometry.tan_angle_sub_mul_norm_of_inner_eq_zero
theorem InnerProductGeometry.tan_angle_sub_mul_norm_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x ≠ 0 ∨ y = 0 → (InnerProductGeometry.angle x (x - y)).tan * ‖x‖ = ‖y‖
This theorem, named `InnerProductGeometry.tan_angle_sub_mul_norm_of_inner_eq_zero`, is a statement within the field of Inner Product Geometry. It states that for any type `V` that is a Normed Additive Commutative Group and an Inner Product Space over the real numbers `ℝ`, and any non-zero vectors `x` and `y` such that their inner product is zero, the tangent of the angle between vector `x` and the vector resulting from subtracting `y` from `x` multiplied by the norm of `x` equals the norm of `y`. In other words, this is a statement about right-angled triangles in the context of Inner Product Spaces: if `x` and `y` are vectors forming a right angle (that is, their inner product is zero), then the length of `y` (the opposite side) is equal to the length of `x` (the adjacent side) multiplied by the tangent of the angle between `x` and `x - y`.
More concisely: For any non-zero vectors `x` and `y` in a real inner product space with zero inner product, the tangent of the angle between `x` and `x-y` is equal to the norm of `y`.
|
EuclideanGeometry.cos_angle_of_angle_eq_pi_div_two
theorem EuclideanGeometry.cos_angle_of_angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
(EuclideanGeometry.angle p₂ p₃ p₁).cos = dist p₃ p₂ / dist p₁ p₃
This theorem, `EuclideanGeometry.cos_angle_of_angle_eq_pi_div_two`, establishes a key property about angles in a right-angled triangle in Euclidean geometry. Specifically, it states that for any given three points `p₁`, `p₂`, and `p₃` which constitute the vertices of the triangle, if the angle at `p₂` (formed by the line segments to `p₁` and `p₃`) is π/2 (which represents a right angle), then the cosine of the angle at `p₃` (formed by the line segments to `p₂` and `p₁`) is equal to the ratio of the distance between `p₃` and `p₂` to the distance between `p₁` and `p₃`. In essence, this theorem is a formal encapsulation of the familiar trigonometric concept that in a right-angled triangle, the cosine of an angle is the ratio of the length of the adjacent side to the length of the hypotenuse.
More concisely: In a right-angled triangle, the cosine of the angle at the vertex opposite the leg is equal to the ratio of the length of that leg to the length of the hypotenuse.
|
EuclideanGeometry.sin_angle_of_angle_eq_pi_div_two
theorem EuclideanGeometry.sin_angle_of_angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
p₁ ≠ p₂ ∨ p₃ ≠ p₂ → (EuclideanGeometry.angle p₂ p₃ p₁).sin = dist p₁ p₂ / dist p₁ p₃
This theorem, `EuclideanGeometry.sin_angle_of_angle_eq_pi_div_two`, states that for any points `p₁`, `p₂`, and `p₃` in a Euclidean space, if the angle at `p₂` (i.e., `EuclideanGeometry.angle p₁ p₂ p₃`) is equal to $\pi/2$ (or in other words, it's a right angle), and either `p₁` is not the same point as `p₂` or `p₃` is not the same point as `p₂`, then the sine of the angle at `p₃` (i.e., `EuclideanGeometry.angle p₂ p₃ p₁`) is equal to the ratio of the distance between `p₁` and `p₂` to the distance between `p₁` and `p₃`. This theorem is essentially describing one of the fundamental properties of right-angled triangles in the context of Euclidean geometry.
More concisely: If the angle between points `p₁`, `p₂`, and `p₃` in a Euclidean space forms a right angle (i.e., `EuclideanGeometry.angle p₁ p₂ p₃ = π/2`), and `p₁ ≠ p₂` and `p₂ ≠ p₃`, then `EuclideanGeometry.angle p₂ p₃ p₁ = sin(π/2) * (dist (p₁, p₂) / dist (p₁, p₃))`. In other words, the sine of a right angle in Euclidean geometry is equal to the ratio of the length of the leg adjacent to the right angle to the length of the hypotenuse.
|
InnerProductGeometry.tan_angle_add_of_inner_eq_zero
theorem InnerProductGeometry.tan_angle_add_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → (InnerProductGeometry.angle x (x + y)).tan = ‖y‖ / ‖x‖
This theorem states that for any right-angled triangle in a real inner product space, if the inner product of two of its vectors, `x` and `y`, is zero (which indicates they are orthogonal), then the tangent of the angle between vector `x` and the sum of vectors `x` and `y` is equal to the ratio of the norm (length) of vector `y` to the norm of vector `x`. This can be interpreted as the trigonometric relation in a right-angled triangle where the tangent of an angle is the ratio of the length of the side opposite the angle to the length of the side adjacent to the angle.
More concisely: For any right-angled triangle in a real inner product space, the tangent of the angle between two orthogonal vectors `x` and `y` is equal to the norm of `y` divided by the norm of `x`.
|
EuclideanGeometry.dist_div_cos_angle_of_angle_eq_pi_div_two
theorem EuclideanGeometry.dist_div_cos_angle_of_angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
p₁ = p₂ ∨ p₃ ≠ p₂ → dist p₃ p₂ / (EuclideanGeometry.angle p₂ p₃ p₁).cos = dist p₁ p₃
This theorem states that in a right-angled triangle, the length of a side, when divided by the cosine of the angle adjacent to that side, is equal to the length of the hypotenuse. This is subject to the condition that the mentioned angle is equal to π/2 (which characterizes the right angle) and that the first and second points defining the angle are not identical, or the second and third points are not identical. In terms of the underlying types, the theorem works in the context of a Euclidean space modelled by an inner product space over the real numbers.
More concisely: In a right-angled triangle, the length of the hypotenuse is equal to the sum of the lengths of the other two sides, each multiplied by the cosine of the respective adjacent angles. (This is the Pythagorean theorem in disguise, with the given condition ensuring the presence of a right angle.)
|
EuclideanGeometry.dist_div_tan_angle_of_angle_eq_pi_div_two
theorem EuclideanGeometry.dist_div_tan_angle_of_angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
p₁ ≠ p₂ ∨ p₃ = p₂ → dist p₁ p₂ / (EuclideanGeometry.angle p₂ p₃ p₁).tan = dist p₃ p₂
This theorem states that in a right-angled triangle (constructed in a Euclidean space), if the angle at a point `p₂` between lines segments to `p₁` and `p₃` equals π/2 (i.e., the angle is a right angle), then the length of the side from `p₁` to `p₂` divided by the tangent of the angle at `p₂` between segments to `p₃` and `p₁` will equal the length of the side from `p₃` to `p₂`, given that `p₁` is not equal to `p₂` or `p₃` is equal to `p₂`. This is a geometric representation of the tangent function in trigonometry: the ratio of the length of the opposite side to the length of the adjacent side in a right triangle.
More concisely: In a right-angled triangle, the length of the hypotenuse is equal to the product of the length of the adjacent side and the tangent of the right angle.
|
InnerProductGeometry.norm_div_tan_angle_sub_of_inner_eq_zero
theorem InnerProductGeometry.norm_div_tan_angle_sub_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x = 0 ∨ y ≠ 0 → ‖y‖ / (InnerProductGeometry.angle x (x - y)).tan = ‖x‖
This theorem states that in a right-angled triangle within an inner product space over the real numbers, if the inner product of two vectors `x` and `y` is zero (implying that they are orthogonal) and `x` is either zero or `y` is non-zero, then the length (norm) of `y` divided by the tangent of the angle between `x` and `x - y` equals the length of `x`.
More concisely: In a right-angled triangle in an inner product space over the real numbers, if vectors `x` and `y` are orthogonal with `x ≠ 0` or `y ≠ 0`, then `||y|| / tan(θ) = ||x||`, where `θ` is the angle between `x` and `x - y`.
|
InnerProductGeometry.norm_div_cos_angle_add_of_inner_eq_zero
theorem InnerProductGeometry.norm_div_cos_angle_add_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x ≠ 0 ∨ y = 0 → ‖x‖ / (InnerProductGeometry.angle x (x + y)).cos = ‖x + y‖
This theorem states that in a right-angled triangle, the length of one side divided by the cosine of the angle adjacent to that side equals the length of the hypotenuse. Here, the triangle is described in a real inner product space, with `x` and `y` as its vectors. Given the condition that the inner product of `x` and `y` equals 0 (which implies that the angle between them is a right angle), and either `x` is non-zero or `y` is zero, it confirms the said geometric relation about a right-angled triangle: the magnitude of `x` divided by the cosine of the angle between `x` and the vector sum of `x` and `y` equals the magnitude of this vector sum.
More concisely: In a right-angled triangle in a real inner product space, the ratio of the length of one side to the cosine of the angle between that side and the hypotenuse is equal to the length of the hypotenuse.
|
InnerProductGeometry.angle_sub_eq_arctan_of_inner_eq_zero
theorem InnerProductGeometry.angle_sub_eq_arctan_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x ≠ 0 → InnerProductGeometry.angle x (x - y) = (‖y‖ / ‖x‖).arctan
This theorem states that in an inner product space over real numbers, if two vectors `x` and `y` are orthogonal (their inner product equals zero) and vector `x` is nonzero, then the undirected angle between vector `x` and the difference of vectors `x` and `y` is equal to the arctangent of the ratio of the norm of `y` to the norm of `x`. This theorem can be interpreted as a generalization of the property of right-angled triangles where the angle can be expressed using arctangent, to vectors in an inner product space.
More concisely: In an inner product space over real numbers, if vectors `x` and `y` are orthogonal and `x` is nonzero, then the angle between `x` and `x-y` is given by the arctangent of the norm of `y` divided by the norm of `x`.
|
InnerProductGeometry.angle_add_lt_pi_div_two_of_inner_eq_zero
theorem InnerProductGeometry.angle_add_lt_pi_div_two_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x ≠ 0 → InnerProductGeometry.angle x (x + y) < Real.pi / 2
This theorem states that in a non-degenerate (meaning no sides have length zero) right-angled triangle, any angle is less than π/2. More specifically, given a real number inner product space and two vectors `x` and `y` from this space such that the inner product of `x` and `y` equals zero (indicating they are orthogonal) and `x` is non-zero, the undirected angle between `x` and `x + y` is less than π/2. Here, the undirected angle between two vectors is defined as the inverse cosine of the inner product of the vectors divided by the product of their norms. π is defined as twice the zero of the cosine function in the interval [1,2].
More concisely: In a non-degenerate right-angled triangle, the angle between any two orthogonal vectors with non-zero length is less than π/2. Equivalently, in an inner product space, the angle between two orthogonal non-zero vectors is given by the inverse cosine of their inner product divided by the product of their norms, resulting in an angle less than π/2.
|
InnerProductGeometry.tan_angle_add_mul_norm_of_inner_eq_zero
theorem InnerProductGeometry.tan_angle_add_mul_norm_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x ≠ 0 ∨ y = 0 → (InnerProductGeometry.angle x (x + y)).tan * ‖x‖ = ‖y‖
This theorem states that, in the context of an inner product space over the real numbers, given any two vectors `x` and `y`, if the inner product of `x` and `y` equals zero, and either `x` is non-zero or `y` is zero, then the tangent of the angle between `x` and `x + y`, multiplied by the norm of `x`, equals the norm of `y`. This is analogous to the geometric property of a right-angled triangle where the tangent of an angle multiplied by the length of the adjacent side equals the length of the opposite side.
More concisely: In an inner product space over the real numbers, if the inner product of non-zero vectors `x` and `y` is zero, then the tangent of the angle between `x` and `x+y` is equal to the norm of `y` divided by the norm of `x`.
|
InnerProductGeometry.angle_add_eq_arccos_of_inner_eq_zero
theorem InnerProductGeometry.angle_add_eq_arccos_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → InnerProductGeometry.angle x (x + y) = (‖x‖ / ‖x + y‖).arccos
This theorem states that in the context of an inner product space over the real numbers, if the inner product of two vectors `x` and `y` is zero, then the undirected angle between the vector `x` and the vector resulting from the addition of `x` and `y` is equal to the inverse cosine of the ratio of the norm of `x` to the norm of the sum of `x` and `y`. This corresponds to the geometric interpretation in a right-angled triangle where the angle is expressed using the inverse cosine (or `arccos`) function.
More concisely: In an inner product space over the real numbers, the cosine of the undirected angle between vectors `x` and `x + y` is equal to the norm of `x` divided by the norm of `x + y`. Therefore, the angle is given by the inverse cosine of this ratio.
|
InnerProductGeometry.angle_sub_eq_arccos_of_inner_eq_zero
theorem InnerProductGeometry.angle_sub_eq_arccos_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → InnerProductGeometry.angle x (x - y) = (‖x‖ / ‖x - y‖).arccos
The theorem `InnerProductGeometry.angle_sub_eq_arccos_of_inner_eq_zero` states that for any normed add commutative group `V` with an inner product space over the real numbers, given two vectors `x` and `y` in `V`, if the inner product of `x` and `y` is zero (which means `x` and `y` are orthogonal), then the angle between `x` and the vector resulting from `x - y` (which forms a right-angled triangle) is equal to the arccosine of the magnitude (norm) of `x` divided by the magnitude of `x - y`. This theorem provides a way to calculate one of the angles in a right-angled triangle formed by two vectors with zero inner product, using the `arccos` function.
More concisely: For any orthogonal vectors `x` and `y` in a real inner product space `V`, the angle between `x` and `x-y` is given by the arccosine of the ratio of the magnitudes of `x` and `x-y`.
|
InnerProductGeometry.tan_angle_sub_of_inner_eq_zero
theorem InnerProductGeometry.tan_angle_sub_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → (InnerProductGeometry.angle x (x - y)).tan = ‖y‖ / ‖x‖
This theorem states that in the context of an inner product space over the real numbers, given two vectors `x` and `y`, if the inner product of `x` and `y` equals zero (which means `x` and `y` are orthogonal), then the tangent of the angle between vector `x` and vector `(x - y)` (which forms a right-angled triangle with `x` and `y`) is equal to the ratio of the norm of `y` and the norm of `x`. This corresponds to the trigonometric concept in a right-angled triangle where the tangent of an angle is the ratio of the lengths of the opposite side to the adjacent side.
More concisely: In an inner product space over the real numbers, the tangent of the angle between vectors `x` and `y` is equal to the norm of `y` divided by the norm of `x`, given that `x` and `y` are orthogonal.
|
EuclideanGeometry.angle_eq_arccos_of_angle_eq_pi_div_two
theorem EuclideanGeometry.angle_eq_arccos_of_angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
EuclideanGeometry.angle p₂ p₃ p₁ = (dist p₃ p₂ / dist p₁ p₃).arccos
The theorem `EuclideanGeometry.angle_eq_arccos_of_angle_eq_pi_div_two` states that in a right-angled triangle with vertices represented by points `p₁`, `p₂`, and `p₃` in a Euclidean space, if the angle at `p₂` between the line segments to `p₁` and `p₃` is π/2 (or equivalently, 90 degrees), then the angle at `p₃` between the line segments to `p₂` and `p₁` can be expressed using the `arccos` function as the ratio of the distance between `p₃` and `p₂` to the distance between `p₁` and `p₃`.
More concisely: In a right-angled triangle, the angle at the vertex opposite the leg of length `d` is equal to the arccosine of the ratio of the length of the other leg to `d`.
|
EuclideanGeometry.tan_angle_of_angle_eq_pi_div_two
theorem EuclideanGeometry.tan_angle_of_angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
(EuclideanGeometry.angle p₂ p₃ p₁).tan = dist p₁ p₂ / dist p₃ p₂
This theorem, named as `EuclideanGeometry.tan_angle_of_angle_eq_pi_div_two`, states that in the context of a Euclidean Geometry with a Normed Additive Commutative Group `V` (a vector space), an Inner Product Space over `V`, a metric space `P` (a point space), and a Normed Additive Torsor over `V` and `P` (which can be thought of as a space of directed line segments or vectors), given three points `p₁, p₂, p₃` such that the undirected angle at `p₂` between line segments to `p₁` and `p₃` is π/2 (which makes a right-angled triangle), the tangent of the angle at `p₂` between line segments to `p₃` and `p₁` is equal to the ratio of the distance between `p₁` and `p₂` to the distance between `p₃` and `p₂`. In other words, in a right-angled triangle, the tangent of an angle is equal to the ratio of the lengths of the sides opposite to, and adjacent to, the angle.
More concisely: In a right-angled triangle, the tangent of the angle at the vertex opposite the right angle is equal to the ratio of the length of the leg adjacent to the angle to the length of the leg opposite to the angle.
|
InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two
theorem InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ InnerProductGeometry.angle x y = Real.pi / 2
This theorem is a vector form of the Pythagorean theorem, in the context of an inner product space. It states that for any two vectors `x` and `y` in a real inner product space, the square of the norm of the difference between `x` and `y` equals the sum of the squares of the norms of `x` and `y` if and only if the undirected angle between `x` and `y` is π/2 (or 90 degrees). Here the norm of a vector is its length, and the undirected angle between two vectors is the angle you would measure if you don't care about direction, which is defined in terms of the inner product of the two vectors.
More concisely: In a real inner product space, the square of the norm of the difference between two vectors is equal to the sum of the squares of their norms if and only if the vectors are orthogonal (have an angle of π/2 or 90 degrees).
|
InnerProductGeometry.angle_add_pos_of_inner_eq_zero
theorem InnerProductGeometry.angle_add_pos_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x = 0 ∨ y ≠ 0 → 0 < InnerProductGeometry.angle x (x + y)
This theorem states that in the context of an inner product space over the real numbers, if we have two vectors x and y such that their inner product is zero, then for any non-zero vector x, the angle between vector x and the sum of vectors x and y is positive. In other words, in a non-degenerate right-angled triangle formed by the vectors x, y, and x+y (since their inner product is zero, they are orthogonal), the angle associated with the non-zero side is positive. This is a property typically associated with the geometric interpretation of vectors and angles in Euclidean space.
More concisely: In an inner product space over the real numbers, if two vectors have zero inner product, then the angle between one of them and their sum is positive.
|
InnerProductGeometry.sin_angle_add_mul_norm_of_inner_eq_zero
theorem InnerProductGeometry.sin_angle_add_mul_norm_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → (InnerProductGeometry.angle x (x + y)).sin * ‖x + y‖ = ‖y‖
This theorem states that for any two vectors `x` and `y` in an inner product space over the real numbers, if the inner product of `x` and `y` is zero, then the sine of the angle between `x` and `x+y` multiplied by the magnitude (norm) of `x+y` equals the magnitude of `y`. This is analogous to the geometric principle in a right-angled triangle where the length of the opposite side equals the length of the hypotenuse times the sine of the included angle.
More concisely: In an inner product space over the real numbers, the norm of `x + y` times the sine of the angle between `x` and `y` equals the norm of `y` when the inner product of `x` and `y` is zero.
|
InnerProductGeometry.angle_sub_lt_pi_div_two_of_inner_eq_zero
theorem InnerProductGeometry.angle_sub_lt_pi_div_two_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x ≠ 0 → InnerProductGeometry.angle x (x - y) < Real.pi / 2
The theorem `InnerProductGeometry.angle_sub_lt_pi_div_two_of_inner_eq_zero` states that in any non-degenerate right-angled triangle, an angle is less than π / 2. This version of the theorem involves subtracting vectors. More specifically, given a real inner product space and two vectors `x` and `y` such that their inner product is zero and `x` is not a zero vector, the undirected angle between the vector `x` and the difference of the vectors `x` and `y` is less than π / 2.
More concisely: In a non-degenerate real inner product space, the angle between a non-zero vector `x` and the difference `x - y` of another vector `y` for which `x` and `y` have inner product equal to zero, is less than π/2.
|
InnerProductGeometry.norm_div_sin_angle_add_of_inner_eq_zero
theorem InnerProductGeometry.norm_div_sin_angle_add_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x = 0 ∨ y ≠ 0 → ‖y‖ / (InnerProductGeometry.angle x (x + y)).sin = ‖x + y‖
This theorem states that in the context of a vector space with an inner product, given two vectors `x` and `y` such that their inner product is zero (which geometrically means that they are orthogonal), and under the condition that vector `x` is either the zero vector or vector `y` is not zero, then the length of vector `y` divided by the sine of the angle between `x` and `x + y` is equal to the length of the vector `x + y`. This result can be interpreted geometrically as a generalization of a property of right-angled triangles.
More concisely: Given a vector space with an inner product, if vectors `x` and `y` are orthogonal with `x ≠ 0`, then $\frac{||y||}{sin(\theta)} = ||x + y||$, where $\theta$ is the angle between `x` and `x + y`.
|
EuclideanGeometry.tan_angle_mul_dist_of_angle_eq_pi_div_two
theorem EuclideanGeometry.tan_angle_mul_dist_of_angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
p₁ = p₂ ∨ p₃ ≠ p₂ → (EuclideanGeometry.angle p₂ p₃ p₁).tan * dist p₃ p₂ = dist p₁ p₂
This theorem states that in a right-angled triangle, if the angle at a point `p₂` is π/2 (i.e., 90 degrees), then the tangent of the angle at `p₂` with `p₃` and `p₁` (in that order), multiplied by the distance between `p₃` and `p₂`, is equal to the distance between `p₁` and `p₂`. This is subject to the condition that `p₁` and `p₂` are not the same point or `p₃` is different from `p₂`. This property is a geometric interpretation of the trigonometric identity involving tangent of an angle in a right-angled triangle.
More concisely: In a right-angled triangle, the tangent of the angle between two vertices, multiplied by the length of the side opposite that angle, equals the length of the hypotenuse if the angle is 90 degrees and the vertices are distinct.
|
InnerProductGeometry.angle_add_eq_arcsin_of_inner_eq_zero
theorem InnerProductGeometry.angle_add_eq_arcsin_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x ≠ 0 ∨ y ≠ 0 → InnerProductGeometry.angle x (x + y) = (‖y‖ / ‖x + y‖).arcsin
This theorem, titled `InnerProductGeometry.angle_add_eq_arcsin_of_inner_eq_zero`, states that for any inner product space over the real numbers, given two vectors `x` and `y`, if the inner product of `x` and `y` equals to zero (which means they are orthogonal to each other) and at least one of the vectors is not a zero vector, then the angle between vector `x` and the vector resulting from the addition of `x` and `y` is equal to the arcsin of the ratio of the norm of `y` to the norm of the vector resulting from the addition of `x` and `y`. Here, the angle is computed using the `InnerProductGeometry.angle` function and the arcsin is computed using the `Real.arcsin` function.
More concisely: If two vectors in an inner product space over the real numbers are orthogonal to each other and at least one is non-zero, then the angle between the first vector and the sum of the two vectors is equal to the arcsine of the ratio of the norm of the second vector to the norm of their sum.
|
InnerProductGeometry.cos_angle_add_of_inner_eq_zero
theorem InnerProductGeometry.cos_angle_add_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → (InnerProductGeometry.angle x (x + y)).cos = ‖x‖ / ‖x + y‖
This theorem states that in the context of an inner product space over the reals with a normed add commutative group, given two vectors `x` and `y`, if the inner product of `x` and `y` is zero (which means that they are orthogonal), then the cosine of the angle between `x` and the vector `x + y` is equal to the ratio of the norm of `x` to the norm of `x + y`. This is analogous to the geometric concept from trigonometry that in a right-angled triangle, the cosine of an angle is the ratio of the adjacent side length to the length of the hypotenuse.
More concisely: In an inner product space over the reals, the cosine of the angle between vectors `x` and `x + y` is equal to the quotient of the norm of `x` by the norm of `x + y`, given that `x` and `y` are orthogonal.
|
InnerProductGeometry.cos_angle_sub_of_inner_eq_zero
theorem InnerProductGeometry.cos_angle_sub_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → (InnerProductGeometry.angle x (x - y)).cos = ‖x‖ / ‖x - y‖
The theorem `InnerProductGeometry.cos_angle_sub_of_inner_eq_zero` states that in an inner product space over the reals, given any two vectors `x` and `y`, if the inner product of `x` and `y` is zero (which implies they are orthogonal), then the cosine of the angle between the vector `x` and the vector `x - y` (which forms a right-angled triangle) is equal to the ratio of the norm of `x` to the norm of `x - y`. This is a geometric interpretation of the Pythagorean theorem in terms of angles and lengths in an inner product space.
More concisely: In an inner product space over the reals, if the inner product of vectors `x` and `y` is zero, then the cosine of the angle between `x` and `x-y` is equal to the quotient of the norm of `x` by the norm of `x-y`.
|
InnerProductGeometry.angle_sub_pos_of_inner_eq_zero
theorem InnerProductGeometry.angle_sub_pos_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x = 0 ∨ y ≠ 0 → 0 < InnerProductGeometry.angle x (x - y)
This theorem states: for any normed add commutative group `V` which is also a real inner product space, and for any two vectors `x` and `y` in this space such that their inner product equals zero, if `x` equals zero or `y` is not equal to zero, then the angle between vector `x` and the difference vector `x - y` (i.e., the vector that points from `y` to `x`) is positive. This can be interpreted as a condition for a non-degenerate right triangle: if the dot product of two vectors is zero, then they are orthogonal and form a right triangle with the origin (unless one of them is a zero vector), and the angle in question is one of the non-right angles of this triangle, which is always positive.
More concisely: If `V` is a real inner product space, `x` and `y` are vectors in `V` with inner product equal to zero, and neither `x` nor `y` is the zero vector, then the angle between `x` and `x - y` is positive.
|
EuclideanGeometry.sin_angle_mul_dist_of_angle_eq_pi_div_two
theorem EuclideanGeometry.sin_angle_mul_dist_of_angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
(EuclideanGeometry.angle p₂ p₃ p₁).sin * dist p₁ p₃ = dist p₁ p₂
This theorem states that in a right-angled triangle with vertices `p₁`, `p₂`, and `p₃`, if the angle at vertex `p₂` (denoted as `EuclideanGeometry.angle p₁ p₂ p₃`) is equal to π/2 (or 90 degrees), then the sine of the angle at `p₃` (denoted as `EuclideanGeometry.angle p₂ p₃ p₁`) multiplied by the distance between `p₁` and `p₃` (the length of the hypotenuse) equals the distance between `p₁` and `p₂` (the length of the opposite side to `p₃`). In other words, this is a formal statement of the well-known trigonometric relationship in a right-angled triangle, commonly known as "sine of an angle is opposite side over hypotenuse".
More concisely: In a right-angled triangle, the sine of the angle opposite the hypotenuse is equal to the ratio of the length of the opposite side to the length of the hypotenuse.
|
EuclideanGeometry.angle_le_pi_div_two_of_angle_eq_pi_div_two
theorem EuclideanGeometry.angle_le_pi_div_two_of_angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 → EuclideanGeometry.angle p₂ p₃ p₁ ≤ Real.pi / 2
This theorem states that in a right-angled triangle, any angle is at most `π / 2`. More specifically, given an arbitrary Normed Additive Commutative Group `V`, an Inner Product Space over `V`, a Metric Space `P`, and a Normed Additive Torsor over `P`, if the undirected angle at `p₂` between the line segments to `p₁` and `p₃` is `π / 2` (which means we have a right angle at `p₂`), then the undirected angle at `p₃` between the line segments to `p₂` and `p₁` is less than or equal to `π / 2`. In simpler terms, if one angle of a triangle is `π / 2`, then the other angles are not greater than `π / 2`, which is a fundamental property of right-angled triangles.
More concisely: In a right-angled triangle, the measure of each angle is at most π/2.
|
InnerProductGeometry.norm_div_cos_angle_sub_of_inner_eq_zero
theorem InnerProductGeometry.norm_div_cos_angle_sub_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x ≠ 0 ∨ y = 0 → ‖x‖ / (InnerProductGeometry.angle x (x - y)).cos = ‖x - y‖
The theorem `InnerProductGeometry.norm_div_cos_angle_sub_of_inner_eq_zero` states that for any real inner product space, if the inner product of two vectors `x` and `y` is zero, and either `x` is not the zero vector or `y` is the zero vector, then the length of vector `x` divided by the cosine of the angle between `x` and `x - y` equals the length of the vector `x - y`. This is akin to a trigonometric property of right-angled triangles, where the length of a side divided by the cosine of the adjacent angle equals the length of the hypotenuse.
More concisely: If the inner product of vectors `x` and `y` is zero, and at least one of them is non-zero, then the length of `x` is equal to the length of `x - y` multiplied by the absolute value of the cosine of the angle between `x` and `x - y`.
|
InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero
theorem InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
⟪x, y⟫_ℝ = 0 → x = 0 ∨ y ≠ 0 → ‖y‖ / (InnerProductGeometry.angle x (x + y)).tan = ‖x‖
The theorem `InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero` states that for any vector space `V` over the real numbers, equipped with a normed additive commutative group structure and an inner product space structure, given two vectors `x` and `y` such that their inner product is `0` and either `x` is the zero vector or `y` is not the zero vector, the magnitude (or norm) of `y` divided by the tangent of the angle between `x` and the vector sum of `x` and `y` equals the magnitude of `x`. This is analogous to the geometric fact in right triangle trigonometry that the length of a side of a right-angled triangle divided by the tangent of the opposite angle equals the length of the adjacent side.
More concisely: For any normed inner product space V over the real numbers, if x and y are vectors with inner product 0 and neither is the zero vector, then ||x|| = ||y|| * tan(angle between x and y + π/2).
|
InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq'
theorem InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq' :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
InnerProductGeometry.angle x y = Real.pi / 2 → ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
This theorem, known as the Pythagorean theorem in vector form, states that for any two vectors `x` and `y` in a real inner product space, if the undirected angle between `x` and `y` is π/2 (i.e., the vectors are orthogonal to each other), then the square of the norm of the difference of the two vectors equals the sum of the squares of the norms of the vectors. In mathematical notation, if the angle between vectors x and y is π/2, then ‖x - y‖² = ‖x‖² + ‖y‖². This is a generalization of the classical Pythagorean theorem for right-angled triangles to the context of inner product spaces.
More concisely: In a real inner product space, if two vectors are orthogonal, then the square of the norm of their difference equals the sum of the squares of their norms.
|
InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq'
theorem InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq' :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
InnerProductGeometry.angle x y = Real.pi / 2 → ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
This is a Pythagorean theorem in vector form. It states that for any two vectors, `x` and `y`, in a real inner product space, if the undirected angle between `x` and `y` is π/2 (i.e., the vectors are orthogonal), then the square of the norm of the sum of `x` and `y` is equal to the sum of the square of the norm of `x` and the square of the norm of `y`. In mathematical terms, if `⟨x, y⟩ = π/2`, then `‖x + y‖² = ‖x‖² + ‖y‖²`, where `⟨., .⟩` denotes the undirected angle between two vectors and `‖.‖` denotes the norm of a vector.
More concisely: In a real inner product space, if two vectors are orthogonal, then the square of their norm-wise sum equals the sum of their squared norms.
|