Power of a point (intersecting chords and secants) #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file proves basic geometrical results about power of a point (intersecting chords and
secants) 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.