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