mathlib documentation

geometry.euclidean.triangle

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 linear_algebra.affine_space.

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

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.

Pythagorean theorem, if-and-only-if vector angle form.

Pythagorean theorem, vector angle form.

Pythagorean theorem, subtracting vectors, if-and-only-if vector angle form.

Pythagorean theorem, subtracting vectors, vector angle form.

Pons asinorum, vector angle form.

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

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

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

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

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 (possible degenerate) triangles in Euclidean affine spaces.

theorem euclidean_geometry.dist_square_eq_dist_square_add_dist_square_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] (p1 p2 p3 : P) :
(dist p1 p3) * dist p1 p3 = (dist p1 p2) * dist p1 p2 + (dist p3 p2) * dist p3 p2 p1 p2 p3 = π / 2

Pythagorean theorem, if-and-only-if angle-at-point form.

theorem euclidean_geometry.dist_square_eq_dist_square_add_dist_square_sub_two_mul_dist_mul_dist_mul_cos_angle {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor 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) * real.cos ( p1 p2 p3)

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

theorem euclidean_geometry.angle_eq_angle_of_dist_eq {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} :
dist p1 p2 = dist p1 p3 p1 p2 p3 = p1 p3 p2

Pons asinorum, angle-at-point form.

theorem euclidean_geometry.dist_eq_of_angle_eq_angle_of_angle_ne_pi {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} :
p1 p2 p3 = p1 p3 p2 p2 p1 p3 πdist p1 p2 = dist p1 p3

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

theorem euclidean_geometry.angle_add_angle_add_angle_eq_pi {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} :
p2 p1p3 p1 p1 p2 p3 + p2 p3 p1 + p3 p1 p2 = π

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