EuclideanGeometry.oangle_add_oangle_add_oangle_eq_pi
theorem EuclideanGeometry.oangle_add_oangle_add_oangle_eq_pi :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [inst_4 : Module.Oriented ℝ V (Fin 2)]
[inst_5 : Fact (FiniteDimensional.finrank ℝ V = 2)] {p1 p2 p3 : P},
p2 ≠ p1 →
p3 ≠ p2 →
p1 ≠ p3 →
EuclideanGeometry.oangle p1 p2 p3 + EuclideanGeometry.oangle p2 p3 p1 + EuclideanGeometry.oangle p3 p1 p2 =
↑Real.pi
This theorem is stating the **sum of the angles of a triangle** theorem from Euclidean Geometry, which states that for any given triangle (which could possibly degenerate into a line) with vertices p1, p2, and p3 in a 2-dimensional vector space V over the real numbers ℝ, the sum of the oriented angles at these points is always equal to π, given that these points are distinct from each other. The oriented angles are calculated using the function `EuclideanGeometry.oangle`. If the underlying space has more than two dimensions, this theorem doesn't apply.
More concisely: In Euclidean geometry, the sum of the oriented angles at distinct points in a triangle is equal to π.
|
InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle
theorem InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * (InnerProductGeometry.angle x y).cos
This theorem is a vector form of the **Law of Cosines** (also known as the cosine rule) in the context of an inner product space over the real numbers. Given two vectors `x` and `y` from a normed add commutative group with a real inner product space, the square of the norm (magnitude) of the difference vector `x - y` equals the sum of the squares of the norms of `x` and `y` minus twice the product of the norms of `x` and `y` and the cosine of the angle between `x` and `y`. This is a fundamental relationship in Euclidean geometry, relating lengths and angles of a triangle, extended here to vectors in an arbitrary inner product space.
More concisely: In an inner product space over the real numbers, the square of the norm of the difference between two vectors is equal to the sum of the squares of their norms minus twice the product of their norms and the cosine of their angle.
|
InnerProductGeometry.cos_angle_sub_add_angle_sub_rev_eq_neg_cos_angle
theorem InnerProductGeometry.cos_angle_sub_add_angle_sub_rev_eq_neg_cos_angle :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
x ≠ 0 →
y ≠ 0 →
(InnerProductGeometry.angle x (x - y) + InnerProductGeometry.angle y (y - x)).cos =
-(InnerProductGeometry.angle x y).cos
This theorem states that in a possibly degenerate triangle (which may flatten to a line) with two nonzero sides represented by vectors `x` and `y`, the cosine of the sum of two angles is equal to the negative of the cosine of the angle between `x` and `y`. Specifically, the two angles in question are the angles of `x` with `x - y` and `y` with `y - x`, respectively. This corresponds to the geometric rule about the cosine of the sum of two angles in a triangle.
More concisely: The cosine of the sum of the angles between vectors `x` and `x-y`, and `y` and `y-x`, in a possibly degenerate triangle is equal to the negative of each other.
|
EuclideanGeometry.dist_eq_of_angle_eq_angle_of_angle_ne_pi
theorem EuclideanGeometry.dist_eq_of_angle_eq_angle_of_angle_ne_pi :
∀ {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},
EuclideanGeometry.angle p1 p2 p3 = EuclideanGeometry.angle p1 p3 p2 →
EuclideanGeometry.angle p2 p1 p3 ≠ Real.pi → dist p1 p2 = dist p1 p3
The theorem `EuclideanGeometry.dist_eq_of_angle_eq_angle_of_angle_ne_pi` is a version of the converse of the Pons Asinorum (Bridge of Asses) in the form of angles at points in Euclidean Geometry. It says that for any three points `p1`, `p2`, and `p3` in a metric space `P` with a normed add torsor `V` and inner product space over the real numbers, if the angle at `p2` between line segments to `p1` and `p3` equals the angle at `p3` between line segments to `p1` and `p2` and this angle is not π, then the distance between `p1` and `p2` equals the distance between `p1` and `p3`. The Pons Asinorum refers to a proposition in Euclid's Elements that states that in an isosceles triangle, the angles at the base are equal.
More concisely: In a metric space with a normed add torsor and inner product over the real numbers, if the angles at points `p2` and `p3` between line segments to a fixed point `p1` are equal and not equal to π, then the distances from `p1` to `p2` and from `p1` to `p3` are equal.
|
InnerProductGeometry.sin_angle_sub_add_angle_sub_rev_eq_sin_angle
theorem InnerProductGeometry.sin_angle_sub_add_angle_sub_rev_eq_sin_angle :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
x ≠ 0 →
y ≠ 0 →
(InnerProductGeometry.angle x (x - y) + InnerProductGeometry.angle y (y - x)).sin =
(InnerProductGeometry.angle x y).sin
This theorem is about the trigonometric identity in the context of angles between vectors in an inner product space. Specifically, for any non-zero vectors `x` and `y` in a real-valued inner product space, the sine of the sum of the angles formed by `x` with `x - y` and `y` with `y - x` is equal to the sine of the angle formed by `x` and `y`. This mirrors the usual geometric property in a possibly degenerate triangle with two given sides being non-zero. This is the vector version of the sine law in trigonometry.
More concisely: In a real- inner product space, the sine of the angle between vectors `x` and `y` is equal to the sine of the angle between `x` and `x-y` as well as the angle between `y` and `y-x`.
|
InnerProductGeometry.sin_angle_add_angle_sub_add_angle_sub_eq_zero
theorem InnerProductGeometry.sin_angle_add_angle_sub_add_angle_sub_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
x ≠ 0 →
y ≠ 0 →
(InnerProductGeometry.angle x y + InnerProductGeometry.angle x (x - y) +
InnerProductGeometry.angle y (y - x)).sin =
0
This theorem states that in the context of an inner product space over the real numbers, given two nonzero vectors `x` and `y`, the sine of the sum of the undirected angles between `x` and `y`, `x` and `x - y`, `y` and `y - x` is zero. This is essentially a vector form of the trigonometric identity explaining the sum of angles in a possibly degenerate triangle, where the two given sides are represented by the vectors `x` and `y`.
More concisely: In an inner product space over the real numbers, the sum of the angles between any two nonzero vectors `x` and `y`, `x` and `x-y`, and `y` and `y-x` is zero in radians.
|
EuclideanGeometry.angle_eq_angle_of_dist_eq
theorem EuclideanGeometry.angle_eq_angle_of_dist_eq :
∀ {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 p2 = dist p1 p3 → EuclideanGeometry.angle p1 p2 p3 = EuclideanGeometry.angle p1 p3 p2
The theorem, commonly known as the Isosceles Triangle Theorem or Pons Asinorum, states that within the context of a Euclidean Geometry that has a Normed Additive Commutative Group, an Inner Product Space over the real numbers, a Metric Space, and a Normed Additive Torsor structure, if two distances between three points (specifically, the distance from point `p1` to `p2` and the distance from point `p1` to `p3`) are equal, then the angle at `p2` between the line segments to `p1` and `p3` is equal to the angle at `p3` between the line segments to `p1` and `p2`. Essentially, in an isosceles triangle where two sides are of equal length, the angles opposite those sides are equal.
More concisely: In a Euclidean geometry with the given structures, if the lengths of two sides of an isosceles triangle are equal, then the angles opposite those sides are equal.
|
EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle
theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle :
∀ {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 -
2 * dist p1 p2 * dist p3 p2 * (EuclideanGeometry.angle p1 p2 p3).cos
This theorem is the Law of Cosines, or the cosine rule, in its angle-at-point form for Euclidean Geometry. Specifically, given three points `p1`, `p2`, and `p3` in a metric space with an associated normed add torsor and inner product space, the square of the distance between `p1` and `p3` is equal to the sum of the squares of the distances from `p1` to `p2` and from `p3` to `p2`, minus twice the product of these distances times the cosine of the angle at `p2` between the line segments to `p1` and `p3`. In mathematical terms, this can be written as $dist(p1, p3)^2 = dist(p1, p2)^2 + dist(p3, p2)^2 - 2 * dist(p1, p2) * dist(p3, p2) * cos(∠ p1 p2 p3)$.
More concisely: The square of the distance between points `p1` and `p3` in a normed add torsor and inner product space is equal to the sum of the squares of the distances from `p1` to `p2` and from `p3` to `p2`, minus twice the product of these distances times the cosine of the angle between `p1` and `p3` measured at `p2`.
|
InnerProductGeometry.angle_sub_eq_angle_sub_rev_of_norm_eq
theorem InnerProductGeometry.angle_sub_eq_angle_sub_rev_of_norm_eq :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
‖x‖ = ‖y‖ → InnerProductGeometry.angle x (x - y) = InnerProductGeometry.angle y (y - x)
This theorem is a vector angle form of **Pons asinorum** (the Bridge of Asses), a famous statement in geometry. In the context of inner product spaces over the real numbers, the theorem states that for any normed add commutative group `V` with an inner product space structure, given two vectors `x` and `y` in `V` such that they have the same norm (`‖x‖ = ‖y‖`), the angle between `x` and the vector resulting from `x - y` is equal to the angle between `y` and the vector resulting from `y - x`. Here, the angle is calculated using the inner product and norms of the vectors according to the definition of `InnerProductGeometry.angle`.
More concisely: In an inner product space over the real numbers, if two vectors have equal norms, then the angle between each vector and the difference between them is equal.
|
EuclideanGeometry.law_cos
theorem EuclideanGeometry.law_cos :
∀ {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 -
2 * dist p1 p2 * dist p3 p2 * (EuclideanGeometry.angle p1 p2 p3).cos
This theorem states the Law of Cosines (or cosine rule) in its angle-at-point form in the context of Euclidean Geometry. Given any three points `p1`, `p2`, and `p3` in a Euclidean space, the square of the distance between `p1` and `p3` is equal to the sum of the squares of the distances from `p1` to `p2` and `p3` to `p2`, minus twice the product of these two distances multiplied by the cosine of the angle at `p2` between the line segments to `p1` and `p3`. In mathematical terms, it can be written as `dist(p1, p3)^2 = dist(p1, p2)^2 + dist(p3, p2)^2 - 2 * dist(p1, p2) * dist(p3, p2) * cos(∠p1p2p3)`.
More concisely: In Euclidean geometry, the square of the distance between two points is equal to the sum of the squares of the distances from each point to a third point, minus twice the product of the distances and the cosine of the angle between them.
|
InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi
theorem InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
InnerProductGeometry.angle x (x - y) = InnerProductGeometry.angle y (y - x) →
InnerProductGeometry.angle x y ≠ Real.pi → ‖x‖ = ‖y‖
This theorem is a vector angle form of the "Converse of Pons Asinorum" in inner product geometry. It states that for any type `V`, which is a normed add commutative group and also an inner product space over real numbers, and for any two vectors `x` and `y` in this space, if the angle between `x` and `x - y` is the same as the angle between `y` and `y - x`, and the angle between `x` and `y` is not equal to π, then the norms (or lengths) of `x` and `y` must be equal. In mathematical terms, if $\angle x(x-y) = \angle y(y-x)$ and $\angle xy \neq \pi$, then $\|x\| = \|y\|$.
More concisely: If the angle between vectors `x` and `x-y` in a real inner product space equals the angle between `y` and `y-x`, and their angle is not equal to π radians, then the vectors have equal norms.
|
EuclideanGeometry.angle_add_angle_add_angle_eq_pi
theorem EuclideanGeometry.angle_add_angle_add_angle_eq_pi :
∀ {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},
p2 ≠ p1 →
p3 ≠ p1 →
EuclideanGeometry.angle p1 p2 p3 + EuclideanGeometry.angle p2 p3 p1 + EuclideanGeometry.angle p3 p1 p2 =
Real.pi
The theorem `EuclideanGeometry.angle_add_angle_add_angle_eq_pi` states that in any triangle, possibly degenerate (where the given vertex is distinct from the others), the sum of the angles at the vertices is equal to π. This holds true for any three points `p1`, `p2`, and `p3` in a Euclidean space, where the points `p1`, `p2`, and `p3` represent the vertices of the triangle. More precisely, the sum of the angle at `p2` between line segments to `p1` and `p3`, the angle at `p3` between line segments to `p2` and `p1`, and the angle at `p1` between line segments to `p3` and `p2` is equal to π. This is a fundamental result in Euclidean geometry often referred to as the angle sum property of a triangle.
More concisely: In a triangle, the sum of the angles at any two vertices is equal to π.
|
EuclideanGeometry.dist_sq_mul_dist_add_dist_sq_mul_dist
theorem EuclideanGeometry.dist_sq_mul_dist_add_dist_sq_mul_dist :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (a b c p : P),
EuclideanGeometry.angle b p c = Real.pi →
dist a b ^ 2 * dist c p + dist a c ^ 2 * dist b p = dist b c * (dist a p ^ 2 + dist b p * dist c p)
**Stewart's Theorem**
The theorem states that for any points `a`, `b`, `c`, and `p` in a Euclidean space with a normed add torsor over a normed add commutative group and an inner product space over the real numbers, if the angle `bpc` is equal to π (indicating that `b`, `p`, and `c` are collinear), then the square of the distance from `a` to `b` times the distance from `c` to `p`, plus the square of the distance from `a` to `c` times the distance from `b` to `p`, equals the distance from `b` to `c` times the sum of the square of the distance from `a` to `p` and the product of the distances from `b` to `p` and `c` to `p`. In mathematical terms, this is $dist(a, b)^2 * dist(c, p) + dist(a, c)^2 * dist(b, p) = dist(b, c) * (dist(a, p)^2 + dist(b, p) * dist(c, p))$ if $angle(b, p, c) = π$.
More concisely: For points `a`, `b`, `c`, and `p` in a Euclidean space with an inner product, if `b`, `p`, and `c` are collinear, then the dot product of the differences of `a` and `b`, and `b` and `c`, and the square of the distance between `a` and `p`, equals the sum of the square of the distance between `a` and `b`, the square of the distance between `a` and `c`, and the product of the distances between `b` and `p`, and `c` and `p`. In other words, $(a-b) \cdot (b-c) = dist(a, b)^2 + dist(a, c)^2 - dist(b, p)^2 - dist(c, p)^2 + 2dist(a, p)dist(b, p)dist(c, p)$.
|
EuclideanGeometry.dist_sq_add_dist_sq_eq_two_mul_dist_midpoint_sq_add_half_dist_sq
theorem EuclideanGeometry.dist_sq_add_dist_sq_eq_two_mul_dist_midpoint_sq_add_half_dist_sq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (a b c : P),
dist a b ^ 2 + dist a c ^ 2 = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2)
**Apollonius's Theorem** states that for any three points `a`, `b`, and `c` in a metric space with an associated inner product space, the square of the distance from `a` to `b` plus the square of the distance from `a` to `c` is equal to twice the sum of the square of the distance from `a` to the midpoint of `b` and `c` and the square of half the distance from `b` to `c`. In mathematical terms, this theorem can be written as: $dist(a, b)^2 + dist(a, c)^2 = 2 * (dist(a, midpoint(b, c))^2 + (dist(b, c) / 2)^2$.
More concisely: The square of the distance between any point and the midpoint of two other points is equal to half the sum of the squares of the distances between the point and each of the other two points.
|
InnerProductGeometry.angle_add_angle_sub_add_angle_sub_eq_pi
theorem InnerProductGeometry.angle_add_angle_sub_add_angle_sub_eq_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
x ≠ 0 →
y ≠ 0 →
InnerProductGeometry.angle x y + InnerProductGeometry.angle x (x - y) + InnerProductGeometry.angle y (y - x) =
Real.pi
This theorem states that in a possibly degenerate vector triangle (where the two given sides are nonzero), the sum of the undirected angles between pairs of sides equals π. More specifically, if `x` and `y` are non-zero vectors in a real inner product space `V`, then the sum of the undirected angle between `x` and `y`, the undirected angle between `x` and the difference of `x` and `y`, and the undirected angle between `y` and the difference of `y` and `x`, will always be equal to π.
More concisely: In a real inner product space, the sum of the angles between any two sides of a possibly degenerate vector triangle formed by vectors x, y, and their difference is equal to π.
|
InnerProductGeometry.cos_angle_add_angle_sub_add_angle_sub_eq_neg_one
theorem InnerProductGeometry.cos_angle_add_angle_sub_add_angle_sub_eq_neg_one :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
x ≠ 0 →
y ≠ 0 →
(InnerProductGeometry.angle x y + InnerProductGeometry.angle x (x - y) +
InnerProductGeometry.angle y (y - x)).cos =
-1
This theorem, named `cos_angle_add_angle_sub_add_angle_sub_eq_neg_one`, is about the vector angle in the context of `InnerProductGeometry`. It states that for any non-zero vectors `x` and `y` in a normed add commutative group `V` equipped with an inner product space over the real numbers, the cosine of the sum of the angle between `x` and `y`, the angle between `x` and the difference of `x` and `y`, and the angle between `y` and the difference of `y` and `x`, is equal to `-1`. This theorem can be seen as a generalization of the geometric fact that in an Euclidean space, the sum of the angles of a triangle is `π`, since the cosine of `π` is `-1`.
More concisely: For any non-zero vectors x and y in a real inner product space, the cosine of the angle between x and y, the angle between x and (x - y), and the angle between y and (y - x) is equal to -1.
|