EuclideanGeometry.inversion_involutive
theorem EuclideanGeometry.inversion_involutive :
∀ {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 : ℝ},
R ≠ 0 → Function.Involutive (EuclideanGeometry.inversion c R)
The theorem `EuclideanGeometry.inversion_involutive` states that for any point `c` and a non-zero radius `R`, the inversion operation `EuclideanGeometry.inversion c R` is an involutive function in a Euclidean Geometry context. In simpler terms, this means that if we perform the inversion operation twice, we get back the original point. The inversion operation here is defined as sending each point `x` to a point `y` such that `y -ᵥ c = (R / dist x c) ^ 2 • (x -ᵥ c)`, where `dist x c` is the distance from `x` to `c`, `•` is the scalar multiplication operation, and `-ᵥ` and `+ᵥ` are the vector subtraction and addition operations, respectively.
More concisely: In a Euclidean geometry context, the inversion operation with respect to a point `c` and radius `R` is an involution, i.e., applying it twice to any point `x` results in the original point `x`.
|
EuclideanGeometry.dist_center_inversion
theorem EuclideanGeometry.dist_center_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 : P) (R : ℝ),
dist c (EuclideanGeometry.inversion c R x) = R ^ 2 / dist c x
This theorem in Euclidean Geometry states that the distance from the center of an inversion to the image of a point under the inversion is equal to the square of the radius divided by the distance from the center to the original point. This formula is surprisingly valid even when the original point is exactly at the center of the inversion. The inversion referred to here is a transformation that maps each point `x` to another point `y` such that the difference vector from `y` to the center `c` is proportional to the square of the ratio of the sphere's radius `R` to the distance from `x` to `c`, times the difference vector from `x` to `c`. This transformation is defined in a general affine space over a field equipped with a metric and an inner product.
More concisely: In Euclidean geometry, the distance from the center of an inversion to its image is equal to the radius squared divided by the original distance to the center.
|
EuclideanGeometry.inversion_self
theorem EuclideanGeometry.inversion_self :
∀ {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 : ℝ), EuclideanGeometry.inversion c R c = c
This theorem states that for any point `c` in a metric space `P` and any real number `R`, the inversion of `c` in a sphere centered at `c` with radius `R` is `c` itself. In other words, the center of a sphere in Euclidean Geometry is invariant under the process of inversion.
The inversion operation is defined such that each point `x` is mapped 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 point `c` in a metric space `P` and real number `R`, the result of inverting `c` in a sphere centered at `c` with radius `R` is `c` itself.
|
EuclideanGeometry.inversion_inversion
theorem EuclideanGeometry.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 : P) {R : ℝ},
R ≠ 0 → ∀ (x : P), EuclideanGeometry.inversion c R (EuclideanGeometry.inversion c R x) = x
The theorem `EuclideanGeometry.inversion_inversion` states that for any point in an affine space with a Euclidean geometry, the double application of inversion in a sphere with non-zero radius returns the original point. More precisely, given a point `x` in the space, and a sphere specified by its center `c` and a non-zero radius `R`, the inversion of `x` with respect to the sphere and then another inversion of the result with respect to the same sphere gets us back to the original point `x`. This inversion operation is defined such that it maps `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`, and in the same direction as the vector from `c` to `x`.
More concisely: For any point `x` in an Euclidean affine space and a sphere with non-zero radius `R` and center `c`, applying two inversions of `x` with respect to `S` results in the original point `x`. In other words, inverting a point `x` twice with respect to a sphere centers at `c` and has radius `R` leaves `x` unchanged.
|
EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist
theorem EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst : NormedAddTorsor V P] (a b c d : P),
dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
**Ptolemy's Inequality**: For any four points (labeled `a`, `b`, `c`, `d`) in a space where distances follow the rules of Euclidean geometry, the product of the distances between points `a` and `c` and between `b` and `d` is less than or equal to the sum of the product of the distances between `a` and `b` and `c` and `d` and the product of the distances between `b` and `c` and `a` and `d`. If these four points form a convex cyclic polygon, this inequality becomes an equality.
More concisely: In Euclidean geometry, the product of the lengths of the sides opposite two non-adjacent vertices of a convex cyclic quadrilateral is greater than or equal to the sum of the products of the lengths of the adjacent sides. If the quadrilateral is convex and cyclic, then equality holds.
|
EuclideanGeometry.dist_inversion_center
theorem EuclideanGeometry.dist_inversion_center :
∀ {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 : P) (R : ℝ),
dist (EuclideanGeometry.inversion c R x) c = R ^ 2 / dist x c
This theorem states that in a Euclidean geometry, the distance from the image of a point under inversion to the center of inversion is equal to the square of the radius of inversion divided by the distance of the original point to the center. This inversion map is defined for every point `x` such that `y -ᵥ c = (R / dist x c) ^ 2 • (x -ᵥ c)`, where `y` is the image of the point `x` under inversion, and `c` and `R` are the center and radius of the sphere of inversion respectively. The formula also holds when the point `x` coincides with the center of inversion `c`.
More concisely: In Euclidean geometry, the distance from a point to the center of inversion under an inversion transformation is equal to the square of the radius of inversion divided by the distance of the point to the center of inversion for points outside the sphere of inversion, and is equal to zero for points on the sphere.
|
EuclideanGeometry.dist_inversion_inversion
theorem 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
This theorem states that for any points `x` and `y` in a given Euclidean space, that are not equal to a specified point `c`, and any real number `R`, the distance between the images of `x` and `y` under an inversion operation, where the inversion is defined with respect to a sphere with center `c` and radius `R`, is equal to `R^2` divided by the product of the distances between `x` and `c` and `y` and `c`, all multiplied by the distance between `x` and `y`. This operation essentially measures how "far" the points `x` and `y` are moved by the inversion operation.
More concisely: For any points `x` and `y` in a Euclidean space, not equal to point `c`, and real number `R`, the distance between the inverted points under an inversion operation with respect to sphere `(c, R)` is `R^2 * (distance(x, c) * distance(y, c)) / (distance(x, y)^2)`.
|