Triangles

This file proves basic geometrical results about distances and angles in (possibly degenerate) triangles in real inner product spaces and Euclidean affine spaces. More specialized results, and results developed for simplices in general rather than just for triangles, are in separate files. Definitions and results that make sense in more general affine spaces rather than just in the Euclidean case go under LinearAlgebra.AffineSpace.

Implementation notes

Results in this file are generally given in a form with only those non-degeneracy conditions needed for the particular result, rather than requiring affine independence of the points of a triangle unnecessarily.

References

• https://en.wikipedia.org/wiki/Law_of_cosines
• https://en.wikipedia.org/wiki/Pons_asinorum
• https://en.wikipedia.org/wiki/Sum_of_angles_of_a_triangle

Geometrical results on triangles in real inner product spaces

This section develops some results on (possibly degenerate) triangles in real inner product spaces, where those definitions and results can most conveniently be developed in terms of vectors and then used to deduce corresponding results for Euclidean affine spaces.

theorem InnerProductGeometry.norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x y : V) : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y)

Law of cosines (cosine rule), vector angle form.

theorem InnerProductGeometry.angle_sub_eq_angle_sub_rev_of_norm_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : ‖x‖ = ‖y‖) : angle x (x - y) = angle y (y - x)

Pons asinorum, vector angle form.

theorem InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (h : angle x (x - y) = angle y (y - x)) (hpi : angle x y ≠ Real.pi) : ‖x‖ = ‖y‖

Converse of pons asinorum, vector angle form.

theorem InnerProductGeometry.cos_angle_sub_add_angle_sub_rev_eq_neg_cos_angle {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : Real.cos (angle x (x - y) + angle y (y - x)) = -Real.cos (angle x y)

The cosine of the sum of two angles in a possibly degenerate triangle (where two given sides are nonzero), vector angle form.

theorem InnerProductGeometry.sin_angle_sub_add_angle_sub_rev_eq_sin_angle {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : Real.sin (angle x (x - y) + angle y (y - x)) = Real.sin (angle x y)

The sine of the sum of two angles in a possibly degenerate triangle (where two given sides are nonzero), vector angle form.

theorem InnerProductGeometry.cos_angle_add_angle_sub_add_angle_sub_eq_neg_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : Real.cos (angle x y + angle x (x - y) + angle y (y - x)) = -1

The cosine of the sum of the angles of a possibly degenerate triangle (where two given sides are nonzero), vector angle form.

theorem InnerProductGeometry.sin_angle_add_angle_sub_add_angle_sub_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : Real.sin (angle x y + angle x (x - y) + angle y (y - x)) = 0

The sine of the sum of the angles of a possibly degenerate triangle (where two given sides are nonzero), vector angle form.

theorem InnerProductGeometry.angle_add_angle_sub_add_angle_sub_eq_pi {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : angle x y + angle x (x - y) + angle y (y - x) = Real.pi

The sum of the angles of a possibly degenerate triangle (where the two given sides are nonzero), vector angle form.

Geometrical results on triangles in Euclidean affine spaces

This section develops some geometrical definitions and results on (possibly degenerate) triangles in Euclidean affine spaces.

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ - 2 * dist p₁ p₂ * dist p₃ p₂ * Real.cos (angle p₁ p₂ p₃)

Law of cosines (cosine rule), angle-at-point form.

theorem EuclideanGeometry.law_cos {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ - 2 * dist p₁ p₂ * dist p₃ p₂ * Real.cos (angle p₁ p₂ p₃)

Alias of EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle.

---

Law of cosines (cosine rule), angle-at-point form.

theorem EuclideanGeometry.angle_eq_angle_of_dist_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : dist p₁ p₂ = dist p₁ p₃) : angle p₁ p₂ p₃ = angle p₁ p₃ p₂

Isosceles Triangle Theorem: Pons asinorum, angle-at-point form.

theorem EuclideanGeometry.dist_eq_of_angle_eq_angle_of_angle_ne_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : angle p₁ p₂ p₃ = angle p₁ p₃ p₂) (hpi : angle p₂ p₁ p₃ ≠ Real.pi) : dist p₁ p₂ = dist p₁ p₃

Converse of pons asinorum, angle-at-point form.

theorem EuclideanGeometry.angle_add_angle_add_angle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h2 : p₂ ≠ p₁) (h3 : p₃ ≠ p₁) : angle p₁ p₂ p₃ + angle p₂ p₃ p₁ + angle p₃ p₁ p₂ = Real.pi

The sum of the angles of a triangle (possibly degenerate, where the given vertex is distinct from the others), angle-at-point.

theorem EuclideanGeometry.oangle_add_oangle_add_oangle_eq_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] {p₁ p₂ p₃ : P} (h21 : p₂ ≠ p₁) (h32 : p₃ ≠ p₂) (h13 : p₁ ≠ p₃) : oangle p₁ p₂ p₃ + oangle p₂ p₃ p₁ + oangle p₃ p₁ p₂ = ↑Real.pi

The sum of the angles of a triangle (possibly degenerate, where the triangle is a line), oriented angles at point.

theorem EuclideanGeometry.dist_sq_mul_dist_add_dist_sq_mul_dist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (a b c p : P) (h : 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.

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [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.

theorem EuclideanGeometry.dist_mul_of_eq_angle_of_dist_mul {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (a b c a' b' c' : P) (r : ℝ) (h : angle a' b' c' = angle a b c) (hab : dist a' b' = r * dist a b) (hcb : dist c' b' = r * dist c b) : dist a' c' = r * dist a c