Theorems · Theorem · geometry

EuclideanGeometry.dist_inversion_inversion

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c x y : P},
  x ≠ c →
    y ≠ c →
      ∀ (R : ℝ),
        dist (EuclideanGeometry.inversion c R x) (EuclideanGeometry.inversion c R y) =
          R ^ 2 / (dist x c * dist y c) * dist x y

Distance between the images of two points under an inversion.

Defined in

Mathlib.Geometry.Euclidean.Inversion.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor