EuclideanGeometry.inversion_mem_perpBisector_inversion_iff
theorem EuclideanGeometry.inversion_mem_perpBisector_inversion_iff :
∀ {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} {R : ℝ},
R ≠ 0 →
x ≠ c →
y ≠ c →
(EuclideanGeometry.inversion c R x ∈ AffineSubspace.perpBisector c (EuclideanGeometry.inversion c R y) ↔
dist x y = dist y c)
The theorem states that in a Euclidean affine space with a normed add commutative group structure and an inner product space over the reals, given a sphere with center `c` and radius `R` that does not equal 0, and for any two distinct points `x` and `y` that are not at the center `c`, the point `x` when inverted in the sphere will lie on the perpendicular bisector of the segment joining `c` and the inversion of `y` in the sphere, if and only if the distance between `x` and `y` is equal to the distance between `y` and `c`. Here, the inversion of a point `x` in the sphere is defined as the point `y` such that `y - c = (R / dist(x, c))^2 * (x - c)`, and the perpendicular bisector of a segment is defined as the subspace of all points equidistant from the endpoints of the segment.
More concisely: In a Euclidean affine space with a normed add commutative group structure and an inner product space over the reals, for any sphere with non-zero radius, distinct points x and y not at the center, and their inversions y' and x' respectively, the points x and y are on the perpendicular bisector of the segment connecting the center and y' if and only if the distance between x and y is equal to the distance between y and the center.
|
EuclideanGeometry.mapsTo_inversion_affineSubspace_of_mem
theorem EuclideanGeometry.mapsTo_inversion_affineSubspace_of_mem :
∀ {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 : P} {R : ℝ} {p : AffineSubspace ℝ P},
c ∈ p → Set.MapsTo (EuclideanGeometry.inversion c R) ↑p ↑p
The theorem `EuclideanGeometry.mapsTo_inversion_affineSubspace_of_mem` states that for any affine subspace `p` in a Euclidean geometry, if the center `c` of an inversion is in `p`, then applying the inversion maps any point in `p` back to a point in `p`. This can be understood as: the inversion transformation, specified by center `c` and radius `R`, preserves the affine subspace `p` that passes through the inversion center `c`. Here, an inversion is defined as a transformation that sends a point `x` to a point `y` such that the vector `y - c` is proportional to the square of the ratio `R / dist(x, c)` times the vector `x - c`, where `R` is the radius of the sphere and `dist(., .)` is the Euclidean distance between two points. The affineness of the subspace ensures that it remains a flat subspace under the inversion.
More concisely: Given an affine subspace `p` and a center `c` in a Euclidean geometry such that `c` is in `p`, the inversion with center `c` maps every point in `p` to another point in `p`.
|
EuclideanGeometry.image_inversion_affineSubspace_of_mem
theorem EuclideanGeometry.image_inversion_affineSubspace_of_mem :
∀ {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 : P} {R : ℝ} {p : AffineSubspace ℝ P},
R ≠ 0 → c ∈ p → EuclideanGeometry.inversion c R '' ↑p = ↑p
This theorem states that for any affine subspace 'p' in a Euclidean space that passes through the center 'c' of a sphere with a non-zero radius 'R', applying the inversion transformation on this subspace will yield the subspace itself. Here, the inversion transformation is defined as sending each point 'x' to a point 'y' such that the vector from 'c' to 'y' is proportional to the square of the ratio of 'R' to the distance from 'x' to 'c' times the vector from 'c' to 'x'.
More concisely: For any affine subspace passing through the center of a sphere in a Euclidean space and having non-zero radius, the inversion transformation maps the subspace to itself.
|
EuclideanGeometry.inversion_mem_perpBisector_inversion_iff'
theorem EuclideanGeometry.inversion_mem_perpBisector_inversion_iff' :
∀ {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} {R : ℝ},
R ≠ 0 →
y ≠ c →
(EuclideanGeometry.inversion c R x ∈ AffineSubspace.perpBisector c (EuclideanGeometry.inversion c R y) ↔
dist x y = dist y c ∧ x ≠ c)
The theorem states that in a Euclidean affine space, given a sphere with a center 'c' and radius 'R' not equal to zero, and two points 'x' and 'y' such that 'y' is not equal to 'c', the inversion of point 'x' with respect to the sphere is on the perpendicular bisector of segment 'cy' where 'y' is the inversion of 'c' with respect to the sphere, if and only if the distance from 'x' to 'y' is equal to the distance from 'y' to 'c' and 'x' is not equal to 'c'. This means the inversion of a sphere passing through the center of inversion to a hyperplane.
More concisely: In a Euclidean affine space, the inversion of point x with respect to a sphere centered at c with radius R is on the perpendicular bisector of the segment cy if and only if x is not equal to c, y is the inversion of c with respect to the sphere, and the distance from x to y is equal to the distance from y to c.
|