Theorems · Theorem · geometry

EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [NormedAddTorsor V P] (a b c d : P), dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d

Ptolemy's inequality: in a quadrangle ABCD, |AC| * |BD| ≤ |AB| * |CD| + |BC| * |AD|. If ABCD is a convex cyclic polygon, then this inequality becomes an equality, see EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical.

Defined in

Mathlib.Geometry.Euclidean.Inversion.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor