# mathlibdocumentation

geometry.euclidean.inversion

# Inversion in an affine space #

In this file we define inversion in a sphere in an affine space. This map sends each point x to the point y such that y -ᵥ c = (R / dist x c) ^ 2 • (x -ᵥ c), where c and R are the center and the radius the sphere.

In many applications, it is convenient to assume that the inversions swaps the center and the point at infinity. In order to stay in the original affine space, we define the map so that it sends center to itself.

Currently, we prove only a few basic lemmas needed to prove Ptolemy's inequality, see euclidean_geometry.mul_dist_le_mul_dist_add_mul_dist.

noncomputable def euclidean_geometry.inversion {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (c : P) (R : ) (x : P) :
P

Inversion in a sphere in an affine space. This map sends each point x to the point y such that y -ᵥ c = (R / dist x c) ^ 2 • (x -ᵥ c), where c and R are the center and the radius the sphere.

Equations
theorem euclidean_geometry.inversion_vsub_center {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (c : P) (R : ) (x : P) :
= (R / c) ^ 2 (x -ᵥ c)
@[simp]
theorem euclidean_geometry.inversion_self {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (c : P) (R : ) :
@[simp]
theorem euclidean_geometry.inversion_dist_center {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (c x : P) :
= x
theorem euclidean_geometry.inversion_of_mem_sphere {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {c x : P} {R : } (h : x ) :
theorem euclidean_geometry.dist_inversion_center {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (c x : P) (R : ) :
= R ^ 2 /

Distance from the image of a point under inversion to the center. This formula accidentally works for x = c.

theorem euclidean_geometry.dist_center_inversion {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (c x : P) (R : ) :
= R ^ 2 /

Distance from the center of an inversion to the image of a point under the inversion. This formula accidentally works for x = c.

@[simp]
theorem euclidean_geometry.inversion_inversion {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (c : P) {R : } (hR : R 0) (x : P) :
theorem euclidean_geometry.inversion_involutive {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (c : P) {R : } (hR : R 0) :
theorem euclidean_geometry.inversion_surjective {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (c : P) {R : } (hR : R 0) :
theorem euclidean_geometry.inversion_injective {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (c : P) {R : } (hR : R 0) :
theorem euclidean_geometry.inversion_bijective {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (c : P) {R : } (hR : R 0) :
theorem euclidean_geometry.dist_inversion_inversion {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {c x y : P} (hx : x c) (hy : y c) (R : ) :
= R ^ 2 / c * c) *

Distance between the images of two points under an inversion.

theorem euclidean_geometry.mul_dist_le_mul_dist_add_mul_dist {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (a b c d : P) :
* * + *

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 euclidean_geometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical.