# Image of a hyperplane under inversion #

In this file we prove that the inversion with center c and radius R ≠ 0 maps a sphere passing through the center to a hyperplane, and vice versa. More precisely, it maps a sphere with center y ≠ c and radius dist y c to the hyperplane AffineSubspace.perpBisector c (EuclideanGeometry.inversion c R y).

The exact statements are a little more complicated because EuclideanGeometry.inversion c R sends the center to itself, not to a point at infinity.

We also prove that the inversion sends an affine subspace passing through the center to itself.

## Keywords #

inversion

theorem EuclideanGeometry.inversion_mem_perpBisector_inversion_iff {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {x : P} {y : P} {R : } (hR : R 0) (hx : x c) (hy : y c) :
dist x y = dist y c

The inversion with center c and radius R maps a sphere passing through the center to a hyperplane.

theorem EuclideanGeometry.inversion_mem_perpBisector_inversion_iff' {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {x : P} {y : P} {R : } (hR : R 0) (hy : y c) :
dist x y = dist y c x c

The inversion with center c and radius R maps a sphere passing through the center to a hyperplane.

theorem EuclideanGeometry.preimage_inversion_perpBisector_inversion {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {y : P} {R : } (hR : R 0) (hy : y c) :
= Metric.sphere y (dist y c) \ {c}
theorem EuclideanGeometry.preimage_inversion_perpBisector {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {y : P} {R : } (hR : R 0) (hy : y c) :
= Metric.sphere (R ^ 2 / dist y c) \ {c}
theorem EuclideanGeometry.image_inversion_perpBisector {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {y : P} {R : } (hR : R 0) (hy : y c) :
= Metric.sphere (R ^ 2 / dist y c) \ {c}
theorem EuclideanGeometry.preimage_inversion_sphere_dist_center {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {y : P} {R : } (hR : R 0) (hy : y c) :
theorem EuclideanGeometry.image_inversion_sphere_dist_center {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {y : P} {R : } (hR : R 0) (hy : y c) :
'' Metric.sphere y (dist y c) = insert c
theorem EuclideanGeometry.mapsTo_inversion_affineSubspace_of_mem {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {R : } {p : } (hp : c p) :
Set.MapsTo p p

Inversion sends an affine subspace passing through the center to itself.

theorem EuclideanGeometry.image_inversion_affineSubspace_of_mem {V : Type u_1} {P : Type u_2} [] [] [] {c : P} {R : } {p : } (hR : R 0) (hp : c p) :
= p

Inversion sends an affine subspace passing through the center to itself.