This file proves basic geometrical results about distances and angles in spheres in real inner product spaces and Euclidean affine spaces.
Main theorems #
mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi: Intersecting Chords Theorem (Freek No. 55).
mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero: Intersecting Secants Theorem.
mul_dist_add_mul_dist_eq_mul_dist_of_cospherical: Ptolemy’s Theorem (Freek No. 95).
TODO: The current statement of Ptolemy’s theorem works around the lack of a "cyclic polygon" concept in mathlib, which is what the theorem statement would naturally use (or two such concepts, since both a strict version, where all vertices must be distinct, and a weak version, where consecutive vertices may be equal, would be useful; Ptolemy's theorem should then use the weak one).
An API needs to be built around that concept, which would include:
- strict cyclic implies weak cyclic,
- weak cyclic and consecutive points distinct implies strict cyclic,
- weak/strict cyclic implies weak/strict cyclic for any subsequence,
- any three points on a sphere are weakly or strictly cyclic according to whether they are distinct,
- any number of points on a sphere intersected with a two-dimensional affine subspace are cyclic in some order,
- a list of points is cyclic if and only if its reversal is,
- a list of points is cyclic if and only if any cyclic permutation is, while other permutations are not when the points are distinct,
- a point P where the diagonals of a cyclic polygon cross exists (and is unique) with weak/strict betweenness depending on weak/strict cyclicity,
- four points on a sphere with such a point P are cyclic in the appropriate order, and so on.
Geometrical results on spheres in real inner product spaces #
This section develops some results on spheres in real inner product spaces, which are used to deduce corresponding results for Euclidean affine spaces.
Geometrical results on spheres in Euclidean affine spaces #
This section develops some results on spheres in Euclidean affine spaces.
P is a point on the line
Q is equidistant from
AP * BP = abs (BQ ^ 2 - PQ ^ 2).
D are cospherical and
P is on both lines
AP * BP = CP * DP.
Intersecting Chords Theorem.
Intersecting Secants Theorem.