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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c x y : P} {R : ℝ} (hR : R ≠ 0) (hx : x ≠ c) (hy : y ≠ c) : inversion c R x ∈ AffineSubspace.perpBisector c (inversion c R y) ↔ 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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c x y : P} {R : ℝ} (hR : R ≠ 0) (hy : y ≠ c) : inversion c R x ∈ AffineSubspace.perpBisector c (inversion c R y) ↔ 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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c y : P} {R : ℝ} (hR : R ≠ 0) (hy : y ≠ c) : inversion c R ⁻¹' ↑(AffineSubspace.perpBisector c (inversion c R y)) = Metric.sphere y (dist y c) \ {c}

theorem EuclideanGeometry.preimage_inversion_perpBisector {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c y : P} {R : ℝ} (hR : R ≠ 0) (hy : y ≠ c) : inversion c R ⁻¹' ↑(AffineSubspace.perpBisector c y) = Metric.sphere (inversion c R y) (R ^ 2 / dist y c) \ {c}

theorem EuclideanGeometry.image_inversion_perpBisector {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c y : P} {R : ℝ} (hR : R ≠ 0) (hy : y ≠ c) : inversion c R '' ↑(AffineSubspace.perpBisector c y) = Metric.sphere (inversion c R y) (R ^ 2 / dist y c) \ {c}

theorem EuclideanGeometry.preimage_inversion_sphere_dist_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c y : P} {R : ℝ} (hR : R ≠ 0) (hy : y ≠ c) : inversion c R ⁻¹' Metric.sphere y (dist y c) = insert c ↑(AffineSubspace.perpBisector c (inversion c R y))

theorem EuclideanGeometry.image_inversion_sphere_dist_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c y : P} {R : ℝ} (hR : R ≠ 0) (hy : y ≠ c) : inversion c R '' Metric.sphere y (dist y c) = insert c ↑(AffineSubspace.perpBisector c (inversion c R y))

theorem EuclideanGeometry.mapsTo_inversion_affineSubspace_of_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {R : ℝ} {p : AffineSubspace ℝ P} (hp : c ∈ p) : Set.MapsTo (inversion c R) ↑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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {c : P} {R : ℝ} {p : AffineSubspace ℝ P} (hR : R ≠ 0) (hp : c ∈ p) : inversion c R '' ↑p = ↑p

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