EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero
theorem EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2}
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {a b c d p : P},
EuclideanGeometry.Cospherical {a, b, c, d} →
a ≠ b →
c ≠ d →
EuclideanGeometry.angle a p b = 0 →
EuclideanGeometry.angle c p d = 0 → dist a p * dist b p = dist c p * dist d p
This is the **Intersecting Secants Theorem**. It states that for any metric space `P` with an associated normed add commutative group `V` and any five points `a`, `b`, `c`, `d`, and `p` in `P`, if the set of points `{a, b, c, d}` is cospherical (meaning they are equidistant from some common point), `a` and `b` are distinct and `c` and `d` are distinct, and if the angle at `p` between `a` and `b` is zero (meaning `a`, `p`, and `b` are collinear) and the angle at `p` between `c` and `d` is also zero (meaning `c`, `p`, and `d` are collinear), then the product of the distance from `a` to `p` and the distance from `b` to `p` equals the product of the distance from `c` to `p` and the distance from `d` to `p`. This is a fundamental theorem in Euclidean geometry.
More concisely: In a metric space with associated normed add commutative group, if five distinct points are cospherical and their corresponding pairs of points form collinear triples, then the product of the distances between each point and the common point is equal for each pair.
|
EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi
theorem EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2}
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {a b c d p : P},
EuclideanGeometry.Cospherical {a, b, c, d} →
EuclideanGeometry.angle a p b = Real.pi →
EuclideanGeometry.angle c p d = Real.pi → dist a p * dist b p = dist c p * dist d p
The **Intersecting Chords Theorem** states that in a Euclidean space with a normed add commutative group structure and an inner product space over the real numbers, given five points (a, b, c, d, p), if the points a, b, c, and d are cospherical (equidistant from some center point), and the undirected angles at point p between the line segments to a and b, and c and d are both equal to pi (π), then the product of the distances from p to a and b is equal to the product of the distances from p to c and d.
More concisely: In a Euclidean space with a normed add commutative group structure and an inner product space over the real numbers, if points a, b, c, d are cospherical with center point p and the angles between line segments ap-b and cp-d are both π, then ap · bp = cd · pd.
|
EuclideanGeometry.mul_dist_eq_abs_sub_sq_dist
theorem EuclideanGeometry.mul_dist_eq_abs_sub_sq_dist :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2}
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {a b p q : P},
(∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)) →
dist a q = dist b q → dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|
This theorem, from Euclidean Geometry, states that if point `P` lies on line `AB` and a point `Q` is equidistant from points `A` and `B`, then the product of the distances from `A` to `P` and from `B` to `P` equals the absolute value of the difference between the square of the distance from `B` to `Q` and the square of the distance from `P` to `Q`. Here, `dist` denotes Euclidean distance, and `-ᵥ` and `•` are vector subtraction and scalar multiplication, respectively, from the normed add-torsor structure on `P`.
More concisely: If point `P` lies on line `AB` and point `Q` is equidistant from points `A` and `B`, then the product of the distances from `P` to `A` and `P` to `B` equals the squared difference between the distances from `B` to `Q` and `P` to `Q`.
|
EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical
theorem EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2}
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {a b c d p : P},
EuclideanGeometry.Cospherical {a, b, c, d} →
(∃ k₁, k₁ ≠ 1 ∧ b -ᵥ p = k₁ • (a -ᵥ p)) →
(∃ k₂, k₂ ≠ 1 ∧ d -ᵥ p = k₂ • (c -ᵥ p)) → dist a p * dist b p = dist c p * dist d p
The theorem states that for a metric space of points equipped with a real inner product space and a torsor structure over the normed add commutative group, if four points `A`, `B`, `C`, `D` are cospherical (i.e., they are all equidistant from some common point), and another point `P` lies on the lines `AB` and `CD` (with certain non-trivial scaling factors), then the product of the Euclidean distances from `P` to `A` and `B` equals the product of the Euclidean distances from `P` to `C` and `D`.
More concisely: If four points in a metric space with an inner product and a torsor structure are cospherical, and a fifth point lies on the lines connecting pairs of them with certain scalings, then the product of the Euclidean distances from the fifth point to each pair is commutative.
|