EuclideanGeometry.mem_sphere
theorem EuclideanGeometry.mem_sphere :
∀ {P : Type u_2} [inst : MetricSpace P] {p : P} {s : EuclideanGeometry.Sphere P},
p ∈ s ↔ dist p s.center = s.radius
This theorem states that for any point `p` and any `Sphere s` in a metric space of type `P`, `p` is in `s` if and only if the distance from `p` to the center of `s` is equal to the radius of `s`. In other words, a point is inside a sphere according to Euclidean Geometry only when its distance from the sphere's center is exactly the sphere's radius.
More concisely: A point is in a sphere in a metric space if and only if the distance from the point to the sphere's center equals the sphere's radius.
|
EuclideanGeometry.Cospherical.affineIndependent_of_ne
theorem EuclideanGeometry.Cospherical.affineIndependent_of_ne :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
EuclideanGeometry.Cospherical {p₁, p₂, p₃} → p₁ ≠ p₂ → p₁ ≠ p₃ → p₂ ≠ p₃ → AffineIndependent ℝ ![p₁, p₂, p₃]
This theorem asserts that for any three distinct points (`p₁`, `p₂`, `p₃`) from a normed add torsor over a normed add commutative group with an inner product space, if these points form a cospherical set — that is, they are all equidistant from some point (like a circle in two dimensions) — then these points are affinely independent. In more technical terms, no nontrivial weighted subtraction of these points, where the sum of weights is zero, results in zero. This is a property that is used to define geometrical concepts such as lines and planes in affine geometry.
More concisely: In a normed add torsor over a normed add commutative group with an inner product space, three distinct points that form a cospherical set are affinely independent.
|
EuclideanGeometry.inner_pos_of_dist_lt_radius
theorem EuclideanGeometry.inner_pos_of_dist_lt_radius :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
p₁ ∈ s → dist p₂ s.center < s.radius → 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫_ℝ
This theorem states that for any given sphere and two distinct points - one on the sphere and the other inside it - the inner product of the vector difference between the points and the vector from the sphere's center to the point on the sphere is always positive. The underlying space here is a normed additively commutative group that has an inner product space structure over real numbers and also has a metric space structure. Also, the space is a normed additive torsor, which means that it allows for the subtraction of points.
More concisely: For any sphere in a normed additive torsor with an inner product space structure over real numbers and a metric space structure, the inner product of the vector difference between a point on the sphere and the sphere's center, and the vector from the sphere's center to the point on the sphere, is positive for any two distinct points, one on the sphere and the other inside it.
|
EuclideanGeometry.cospherical_iff_exists_sphere
theorem EuclideanGeometry.cospherical_iff_exists_sphere :
∀ {P : Type u_2} [inst : MetricSpace P] {ps : Set P},
EuclideanGeometry.Cospherical ps ↔ ∃ s, ps ⊆ Metric.sphere s.center s.radius
This theorem states that within a metric space, a set of points is cospherical (meaning the points are all equidistant from a certain point) if and only if these points lie within a particular sphere. Concretely, for any set of points "ps" in the metric space, it is cospherical if there exists a sphere such that all points in "ps" are included in this sphere (i.e., the distance from each point in "ps" to the center of the sphere is equal to the sphere's radius).
More concisely: A set of points in a metric space is cospherical if and only if they lie within a sphere with equal distances to its center for each point in the set.
|
EuclideanGeometry.inner_pos_or_eq_of_dist_le_radius
theorem EuclideanGeometry.inner_pos_or_eq_of_dist_le_radius :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
p₁ ∈ s → dist p₂ s.center ≤ s.radius → 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫_ℝ ∨ p₁ = p₂
This theorem states that given a sphere in Euclidean geometry, if we consider a point on this sphere and another point that is not outside of the sphere, then the inner product between the vector difference of these two points and the radius vector of the sphere is either positive or the two points are the same. This is true for all points and spheres in a normed add-torsor, which is a metric space equipped with a normed add commutative group structure and an inner product space over the real numbers.
More concisely: Given a sphere in a normed add-torsor with an inner product, for any two points on the sphere, the inner product of the vector difference between them and the radius vector is non-negative (zero if and only if the points are identical).
|
EuclideanGeometry.Cospherical.affineIndependent
theorem EuclideanGeometry.Cospherical.affineIndependent :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : Set P},
EuclideanGeometry.Cospherical s →
∀ {p : Fin 3 → P}, Set.range p ⊆ s → Function.Injective p → AffineIndependent ℝ p
This theorem states that any three points in a cospherical set are affinely independent. In more detail, given a set of points in a Euclidean space that are all equidistant from some point (i.e., they are cospherical), if we take any three distinct points from this set (represented as a function from the finite set of size 3 to the points), then these three points are affinely independent. Here, affinely independent means that no nontrivial weighted sum of the vectors from one fixed point to the three points is zero, where the weights sum to zero. This property is important for many geometric and algebraic computations. The theorem assumes that the mapping from the finite set to the points is injective, meaning each different element in the domain is mapped to a different point.
More concisely: Given a set of three distinct, cospherical points in a Euclidean space, they are affinely independent.
|
EuclideanGeometry.Concyclic.subset
theorem EuclideanGeometry.Concyclic.subset :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
[inst_3 : NormedAddTorsor V P] {ps₁ ps₂ : Set P},
ps₁ ⊆ ps₂ → EuclideanGeometry.Concyclic ps₂ → EuclideanGeometry.Concyclic ps₁
This theorem states that for any two sets of points `ps₁` and `ps₂` in a normed add-torsor Euclidean geometry, if `ps₁` is a subset of `ps₂` (i.e., `ps₁ ⊆ ps₂`) and `ps₂` is a concyclic set (meaning that all the points in the set lie on the same circle), then `ps₁` is also a concyclic set. In simpler terms, it means that if we have a circle with some points on it and we take a subset of those points, those points will still be on the same circle.
More concisely: If a subset of concyclic points in a normed add-torsor Euclidean geometry is contained in a larger concyclic set, then the smaller set is also concyclic.
|
EuclideanGeometry.Cospherical.affineIndependent_of_mem_of_ne
theorem EuclideanGeometry.Cospherical.affineIndependent_of_mem_of_ne :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : Set P},
EuclideanGeometry.Cospherical s →
∀ {p₁ p₂ p₃ : P}, p₁ ∈ s → p₂ ∈ s → p₃ ∈ s → p₁ ≠ p₂ → p₁ ≠ p₃ → p₂ ≠ p₃ → AffineIndependent ℝ ![p₁, p₂, p₃]
This theorem states that in a Euclidean geometry, any three distinct points (p₁, p₂, p₃) from a cospherical set S (a set of points that are all equidistant from some center point) are affinely independent. Affinely independent points are such that no non-trivial weighted subtraction (where the sum of weights equals zero) equals zero. In other words, these three points do not lie on the same straight line in the space defined by the geometry.
More concisely: In a Euclidean geometry, any three distinct points from a cospherical set are affinely independent.
|
EuclideanGeometry.sbtw_of_collinear_of_dist_center_lt_radius
theorem EuclideanGeometry.sbtw_of_collinear_of_dist_center_lt_radius :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
Collinear ℝ {p₁, p₂, p₃} → p₁ ∈ s → dist p₂ s.center < s.radius → p₃ ∈ s → p₁ ≠ p₃ → Sbtw ℝ p₁ p₂ p₃
The theorem `EuclideanGeometry.sbtw_of_collinear_of_dist_center_lt_radius` states that given three collinear points (in a real number space with a normed add commutative group structure and inner product space), where two points are on a sphere and one point is inside the sphere, if the distance between the inside point and the center of the sphere is less than the radius of the sphere, and the point inside the sphere is not the same as the one on the sphere, then the point inside the sphere is strictly between the two points on the sphere. This theorem is part of Euclidean Geometry in the context of a metric space and a normed add torsor.
More concisely: Given three collinear points in a Euclidean space, if two points lie on a sphere and the distance of the third point (not on the sphere) to the sphere's center is less than the sphere's radius, then the third point strictly lies between the other two points on the sphere.
|
EuclideanGeometry.concyclic_empty
theorem EuclideanGeometry.concyclic_empty :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
[inst_3 : NormedAddTorsor V P], EuclideanGeometry.Concyclic ∅
This theorem states that the empty set is concyclic. In the context of Euclidean Geometry, a set of points is said to be concyclic if they can all lie on the circumference of a single circle. Therefore, this theorem is saying that no matter what the types of the normed add commutative group, normed space, metric space, and normed add torsor are, the empty set can always be considered as concyclic.
More concisely: The empty set is considered concyclic in the context of Euclidean Geometry, regardless of the underlying normed add commutative group, normed space, metric space, and normed add torsor structures.
|
EuclideanGeometry.concyclic_singleton
theorem EuclideanGeometry.concyclic_singleton :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
[inst_3 : NormedAddTorsor V P] (p : P), EuclideanGeometry.Concyclic {p}
This theorem states that in Euclidean Geometry, a single point is considered to be concyclic. The theorem applies to any point 'p' in a normed add torsor, where the torsor is a metric space over a real number normed space. Essentially, the theorem implies that a single point can be considered as a degenerate circle (a circle with a radius of zero).
More concisely: In Euclidean Geometry, any point is considered a degenerate concyclic point in a normed additive torsor.
|
EuclideanGeometry.concyclic_pair
theorem EuclideanGeometry.concyclic_pair :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
[inst_3 : NormedAddTorsor V P] (p₁ p₂ : P), EuclideanGeometry.Concyclic {p₁, p₂}
This theorem states that any pair of points in a Euclidean space are concyclic. In other words, it is always possible to find a circle that passes through both points. This theorem is applicable in any normed additive commutative group and any normed space over the reals, with the points being in any metric space that forms a normed add-torsor with the group.
More concisely: In any normed additive commutative group and normed space over the reals, any two points have the property that there exists a circle passing through them.
|
EuclideanGeometry.cospherical_def
theorem EuclideanGeometry.cospherical_def :
∀ {P : Type u_2} [inst : MetricSpace P] (ps : Set P),
EuclideanGeometry.Cospherical ps ↔ ∃ center radius, ∀ p ∈ ps, dist p center = radius
The theorem `EuclideanGeometry.cospherical_def` provides the definition of Cospherical in the context of Euclidean Geometry. It states that for any set of points `ps` in a metric space `P`, the set `ps` is considered cospherical if and only if there exists a center point and a radius such that the distance between every point in the set `ps` and the center is equal to the radius. In two dimensions, this concept is analogous to the points being concyclic.
More concisely: A set of points in a metric space is cospherical if and only if there exists a center point and a radius such that the distance between each point in the set and the center is equal to the radius.
|
EuclideanGeometry.Cospherical.subset
theorem EuclideanGeometry.Cospherical.subset :
∀ {P : Type u_2} [inst : MetricSpace P] {ps₁ ps₂ : Set P},
ps₁ ⊆ ps₂ → EuclideanGeometry.Cospherical ps₂ → EuclideanGeometry.Cospherical ps₁
This theorem states that if we have a subset of a cospherical set in a metric space, then the subset is also cospherical. In other words, if we have a set of points that are all equidistant from a certain point (the definition of a cospherical set), then any subset of this set will also have all its points equidistant from the same point. The type of the points is arbitrary, it could be, for instance, real numbers or complex numbers, and the metric space they inhabit is also arbitrary. The theorem captures an intuitive geometrical property: if all points of a set lie on a sphere (in three dimensions), or a circle (in two dimensions), then any subset of these points also lies on the same sphere or circle.
More concisely: If a subset of a cospherical set in a metric space is non-empty, then it is also a cospherical set with respect to the same center point.
|
EuclideanGeometry.cospherical_pair
theorem EuclideanGeometry.cospherical_pair :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
[inst : NormedAddTorsor V P] (p₁ p₂ : P), EuclideanGeometry.Cospherical {p₁, p₂}
The theorem `EuclideanGeometry.cospherical_pair` states that for any two points `p₁` and `p₂` in a normed space over the real numbers, the set containing these two points is cospherical. Here, being cospherical means that these two points are equidistant from some specific point, which can be considered as the center of a sphere.
More concisely: For any two points `p₁` and `p₂` in a normed space over the real numbers, there exists a point `c` such that `d(p₁, c) = d(p₂, c)`, where `d` denotes the distance function.
|
EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere'
theorem EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere' :
∀ {P : Type u_2} [inst : MetricSpace P] {p₁ p₂ : P} {s : EuclideanGeometry.Sphere P},
p₁ ∈ s → p₂ ∈ s → dist s.center p₁ = dist s.center p₂
This theorem, named `EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere'`, states that for any metric space `P` and any two points `p₁` and `p₂` in `P`, if both points belong to the same sphere `s`, then the distances from the center of the sphere to `p₁` and `p₂` are equal. This theorem aligns with our intuitive understanding of a sphere, as it basically states that all points on a sphere's surface are equidistant from the sphere's center.
More concisely: In a metric space, the distances from the center of a sphere to any two points in the sphere are equal.
|
EuclideanGeometry.inner_vsub_vsub_of_mem_sphere_of_mem_sphere
theorem EuclideanGeometry.inner_vsub_vsub_of_mem_sphere_of_mem_sphere :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {p₁ p₂ : P} {s₁ s₂ : EuclideanGeometry.Sphere P},
p₁ ∈ s₁ → p₂ ∈ s₁ → p₁ ∈ s₂ → p₂ ∈ s₂ → ⟪s₂.center -ᵥ s₁.center, p₂ -ᵥ p₁⟫_ℝ = 0
This theorem states that in a Euclidean geometry, if two points `p₁` and `p₂` are present on two spheres `s₁` and `s₂`, then the vector that connects the centers of these two spheres is orthogonal (perpendicular) to the vector connecting `p₁` and `p₂`. This is a version of the theorem `inner_vsub_vsub_of_dist_eq_of_dist_eq` specifically for spheres. In a two-dimensional case, this can be visualized as the diagonals of a kite being perpendicular to each other.
More concisely: In Euclidean geometry, the vector connecting the centers of two spheres is orthogonal to the vector connecting any two points on their respective surfaces.
|
EuclideanGeometry.cospherical_singleton
theorem EuclideanGeometry.cospherical_singleton :
∀ {P : Type u_2} [inst : MetricSpace P] (p : P), EuclideanGeometry.Cospherical {p}
The theorem `EuclideanGeometry.cospherical_singleton` states that for any point 'p' in a metric space 'P', the set containing only 'p' is cospherical. In other words, a single point is always cospherical, as it is trivially equidistant from itself.
More concisely: In a metric space, the singleton set of any point is a cospherical set.
|
EuclideanGeometry.wbtw_of_collinear_of_dist_center_le_radius
theorem EuclideanGeometry.wbtw_of_collinear_of_dist_center_le_radius :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
Collinear ℝ {p₁, p₂, p₃} → p₁ ∈ s → dist p₂ s.center ≤ s.radius → p₃ ∈ s → p₁ ≠ p₃ → Wbtw ℝ p₁ p₂ p₃
The theorem `EuclideanGeometry.wbtw_of_collinear_of_dist_center_le_radius` states that given three points (`p₁`, `p₂`, `p₃`) in a Euclidean geometry where `p₁` and `p₃` are on a sphere (`s`) and `p₂` is not outside the sphere (the distance from `p₂` to the center of the sphere is less than or equal to the sphere's radius), and these three points are collinear (lie on the same straight line), then point `p₂` is weakly between points `p₁` and `p₃`. The condition of weakly betweenness implies that `p₂` lies in the affine segment between `p₁` and `p₃`. The theorem also assumes that `p₁` and `p₃` are distinct points.
More concisely: Given three distinct points `p₁`, `p₂`, and `p₃` in Euclidean geometry where `p₁` and `p₃` lie on a sphere with center `C` and radius `r`, and the distance from `p₂` to `C` is less than or equal to `r`, if `p₁`, `p₂`, and `p₃` are collinear, then `p₂` is weakly between `p₁` and `p₃`.
|
EuclideanGeometry.cospherical_empty
theorem EuclideanGeometry.cospherical_empty :
∀ {P : Type u_2} [inst : MetricSpace P] [inst_1 : Nonempty P], EuclideanGeometry.Cospherical ∅
This theorem states that the empty set is cospherical in any metric space. In other words, for any type `P` which has a notion of metric (or distance), and which is nonempty, the empty set of points in `P` is considered cospherical. This logically holds because the condition of all points in the set being equidistant from a certain point is trivially satisfied when there are no points in the set.
More concisely: In any metric space, the empty set is cospherical.
|
EuclideanGeometry.Sphere.cospherical
theorem EuclideanGeometry.Sphere.cospherical :
∀ {P : Type u_2} [inst : MetricSpace P] (s : EuclideanGeometry.Sphere P),
EuclideanGeometry.Cospherical (Metric.sphere s.center s.radius)
The theorem states that for any sphere in a Euclidean Geometry, the set of points on the sphere is cospherical. In other words, all points on the surface of the sphere are equidistant from the sphere's center. This distance is equal to the radius of the sphere. This would be true for any sphere in any metric space.
More concisely: In a Euclidean geometry, the set of points on a sphere is equidistant from its center, with this distance equal to the sphere's radius.
|
EuclideanGeometry.eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two
theorem EuclideanGeometry.eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [inst_4 : FiniteDimensional ℝ V],
FiniteDimensional.finrank ℝ V = 2 →
∀ {s₁ s₂ : EuclideanGeometry.Sphere P} {p₁ p₂ p : P},
s₁ ≠ s₂ → p₁ ≠ p₂ → p₁ ∈ s₁ → p₂ ∈ s₁ → p ∈ s₁ → p₁ ∈ s₂ → p₂ ∈ s₂ → p ∈ s₂ → p = p₁ ∨ p = p₂
The theorem `EuclideanGeometry.eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two` states that in a two-dimensional Euclidean space, which is an inner product space over the real numbers, and has finite dimension equal to 2, if we have two distinct spheres and three distinct points, with each point belonging to each sphere, then one of the three points must coincide with one of the other two points. Thus, two spheres can intersect at most at two distinct points in this two-dimensional space.
More concisely: In a 2-dimensional Euclidean space with finite dimension over the real numbers, if two distinct spheres each contain three distinct points, then at least two of those points are identical.
|
EuclideanGeometry.inner_nonneg_of_dist_le_radius
theorem EuclideanGeometry.inner_nonneg_of_dist_le_radius :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
p₁ ∈ s → dist p₂ s.center ≤ s.radius → 0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫_ℝ
This theorem states that given a point on a sphere and another point that is not outside the sphere, the inner product of the vector between these two points and the vector from the point on the sphere to the center of the sphere is always nonnegative. The theorem is set in the context of Euclidean Geometry and uses inner product space and metric space structures, and also involves a normed add torsor, which allows for affine combinations of points.
More concisely: Given two points on a sphere in Euclidean space, the inner product of the vector between them and the vector from the point on the sphere to the sphere's center is nonnegative.
|
EuclideanGeometry.eq_of_mem_sphere_of_mem_sphere_of_mem_of_finrank_eq_two
theorem EuclideanGeometry.eq_of_mem_sphere_of_mem_sphere_of_mem_of_finrank_eq_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P}
[inst_4 : FiniteDimensional ℝ ↥s.direction],
FiniteDimensional.finrank ℝ ↥s.direction = 2 →
∀ {s₁ s₂ : EuclideanGeometry.Sphere P} {p₁ p₂ p : P},
s₁.center ∈ s →
s₂.center ∈ s →
p₁ ∈ s →
p₂ ∈ s →
p ∈ s →
s₁ ≠ s₂ → p₁ ≠ p₂ → p₁ ∈ s₁ → p₂ ∈ s₁ → p ∈ s₁ → p₁ ∈ s₂ → p₂ ∈ s₂ → p ∈ s₂ → p = p₁ ∨ p = p₂
This theorem in Lean 4 states that in a two-dimensional subspace, which also contains the centers of two spheres, these spheres can intersect at most at two points. Specifically, if the subspace is of rank two and both sphere centers are in the subspace, and we have three points, where all three points are in both spheres and in the subspace, and the first two points aren't the same and the two spheres aren't the same either, then the third point must be either the first point or the second point. In simpler terms, it's a specific scenario of the more general fact that two spheres intersect in at most two points.
More concisely: In a two-dimensional subspace containing the centers of two distinct spheres, at most two points from each sphere can lie in the subspace and be mutual points between the spheres.
|
EuclideanGeometry.Sphere.ext
theorem EuclideanGeometry.Sphere.ext :
∀ {P : Type u_2} {inst : MetricSpace P} (x y : EuclideanGeometry.Sphere P),
x.center = y.center → x.radius = y.radius → x = y
This theorem, named `EuclideanGeometry.Sphere.ext`, states that for any metric space `P`, if two spheres in this space have the same center and the same radius, then they are indeed the same sphere. In other words, in Euclidean geometry, a sphere is uniquely defined by its center and radius.
More concisely: In any metric space, two spheres with identical centers and radii are equal.
|