Theorems · Theorem · geometry

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} →
    p ∈ line[ℝ, a, b] → p ∈ line[ℝ, c, d] → dist a p * dist b p = dist c p * dist d p

If A, B, C, D are cospherical and P is on both lines AB and CD, then AP * BP = CP * DP.

Defined in

Mathlib.Geometry.Euclidean.Sphere.Power

Cited by

2 results in Mathlib

Foundations

Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor