# mathlib3documentation

geometry.euclidean.sphere.basic

# Spheres #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines and proves basic results about spheres and cospherical sets of points in Euclidean affine spaces.

## Main definitions #

• euclidean_geometry.sphere bundles a center and a radius.

• euclidean_geometry.cospherical is the property of a set of points being equidistant from some point.

• euclidean_geometry.concyclic is the property of a set of points being cospherical and coplanar.

theorem euclidean_geometry.sphere.ext {P : Type u_2} {_inst_1 : metric_space P} (x y : euclidean_geometry.sphere P) (h : x.center = y.center) (h_1 : x.radius = y.radius) :
x = y
@[ext]
structure euclidean_geometry.sphere (P : Type u_2) [metric_space P] :
Type u_2
• center : P

A sphere P bundles a center and radius. This definition does not require the radius to be positive; that should be given as a hypothesis to lemmas that require it.

Instances for euclidean_geometry.sphere
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem euclidean_geometry.sphere.mk_center {P : Type u_2} [metric_space P] (c : P) (r : ) :
{center := c, radius := r}.center = c
theorem euclidean_geometry.sphere.mk_radius {P : Type u_2} [metric_space P] (c : P) (r : ) :
@[simp]
theorem euclidean_geometry.sphere.coe_mk {P : Type u_2} [metric_space P] (c : P) (r : ) :
{center := c, radius := r} =
@[simp]
theorem euclidean_geometry.sphere.mem_coe {P : Type u_2} [metric_space P] {p : P}  :
p s p s
theorem euclidean_geometry.mem_sphere {P : Type u_2} [metric_space P] {p : P}  :
theorem euclidean_geometry.mem_sphere' {P : Type u_2} [metric_space P] {p : P}  :
theorem euclidean_geometry.subset_sphere {P : Type u_2} [metric_space P] {ps : set P}  :
ps s (p : P), p ps p s
theorem euclidean_geometry.dist_of_mem_subset_sphere {P : Type u_2} [metric_space P] {p : P} {ps : set P} (hp : p ps) (hps : ps s) :
theorem euclidean_geometry.dist_of_mem_subset_mk_sphere {P : Type u_2} [metric_space P] {p c : P} {ps : set P} {r : } (hp : p ps) (hps : ps {center := c, radius := r}) :
= r
theorem euclidean_geometry.sphere.ne_iff {P : Type u_2} [metric_space P] {s₁ s₂ : euclidean_geometry.sphere P} :
theorem euclidean_geometry.sphere.center_eq_iff_eq_of_mem {P : Type u_2} [metric_space P] {s₁ s₂ : euclidean_geometry.sphere P} {p : P} (hs₁ : p s₁) (hs₂ : p s₂) :
s₁.center = s₂.center s₁ = s₂
theorem euclidean_geometry.sphere.center_ne_iff_ne_of_mem {P : Type u_2} [metric_space P] {s₁ s₂ : euclidean_geometry.sphere P} {p : P} (hs₁ : p s₁) (hs₂ : p s₂) :
s₁.center s₂.center s₁ s₂
theorem euclidean_geometry.dist_center_eq_dist_center_of_mem_sphere {P : Type u_2} [metric_space P] {p₁ p₂ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) :
theorem euclidean_geometry.dist_center_eq_dist_center_of_mem_sphere' {P : Type u_2} [metric_space P] {p₁ p₂ : P} (hp₁ : p₁ s) (hp₂ : p₂ s) :
p₁ = p₂
def euclidean_geometry.cospherical {P : Type u_2} [metric_space P] (ps : set P) :
Prop

A set of points is cospherical if they are equidistant from some point. In two dimensions, this is the same thing as being concyclic.

Equations
theorem euclidean_geometry.cospherical_def {P : Type u_2} [metric_space P] (ps : set P) :
(center : P) (radius : ), (p : P), p ps center = radius

The definition of cospherical.

A set of points is cospherical if and only if they lie in some sphere.

The set of points in a sphere is cospherical.

theorem euclidean_geometry.cospherical.subset {P : Type u_2} [metric_space P] {ps₁ ps₂ : set P} (hs : ps₁ ps₂) (hc : euclidean_geometry.cospherical ps₂) :

A subset of a cospherical set is cospherical.

The empty set is cospherical.

A single point is cospherical.

theorem euclidean_geometry.cospherical_pair {V : Type u_1} {P : Type u_2} [ V] [metric_space P] [ P] (p₁ p₂ : P) :

Two points are cospherical.

structure euclidean_geometry.concyclic {V : Type u_1} {P : Type u_2} [ V] [metric_space P] [ P] (ps : set P) :
Prop
• cospherical :
• coplanar : ps

A set of points is concyclic if it is cospherical and coplanar. (Most results are stated directly in terms of cospherical instead of using concyclic.)

theorem euclidean_geometry.concyclic.subset {V : Type u_1} {P : Type u_2} [ V] [metric_space P] [ P] {ps₁ ps₂ : set P} (hs : ps₁ ps₂) (h : euclidean_geometry.concyclic ps₂) :

A subset of a concyclic set is concyclic.

theorem euclidean_geometry.concyclic_empty {V : Type u_1} {P : Type u_2} [ V] [metric_space P] [ P] :

The empty set is concyclic.

theorem euclidean_geometry.concyclic_singleton {V : Type u_1} {P : Type u_2} [ V] [metric_space P] [ P] (p : P) :

A single point is concyclic.

theorem euclidean_geometry.concyclic_pair {V : Type u_1} {P : Type u_2} [ V] [metric_space P] [ P] (p₁ p₂ : P) :

Two points are concyclic.

theorem euclidean_geometry.cospherical.affine_independent {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {s : set P} {p : fin 3 P} (hps : s) (hpi : function.injective p) :

Any three points in a cospherical set are affinely independent.

theorem euclidean_geometry.cospherical.affine_independent_of_mem_of_ne {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {s : set P} {p₁ p₂ p₃ : P} (h₁ : p₁ s) (h₂ : p₂ s) (h₃ : p₃ s) (h₁₂ : p₁ p₂) (h₁₃ : p₁ p₃) (h₂₃ : p₂ p₃) :
![p₁, p₂, p₃]

Any three points in a cospherical set are affinely independent.

theorem euclidean_geometry.cospherical.affine_independent_of_ne {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (hs : euclidean_geometry.cospherical {p₁, p₂, p₃}) (h₁₂ : p₁ p₂) (h₁₃ : p₁ p₃) (h₂₃ : p₂ p₃) :
![p₁, p₂, p₃]

The three points of a cospherical set are affinely independent.

theorem euclidean_geometry.inner_vsub_vsub_of_mem_sphere_of_mem_sphere {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ : P} {s₁ s₂ : euclidean_geometry.sphere P} (hp₁s₁ : p₁ s₁) (hp₂s₁ : p₂ s₁) (hp₁s₂ : p₁ s₂) (hp₂s₂ : p₂ s₂) :
has_inner.inner (s₂.center -ᵥ s₁.center) (p₂ -ᵥ p₁) = 0

Suppose that p₁ and p₂ lie in spheres s₁ and s₂. Then the vector between the centers of those spheres is orthogonal to that between p₁ and p₂; this is a version of inner_vsub_vsub_of_dist_eq_of_dist_eq for bundled spheres. (In two dimensions, this says that the diagonals of a kite are orthogonal.)

theorem euclidean_geometry.eq_of_mem_sphere_of_mem_sphere_of_mem_of_finrank_eq_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {s : P} (hd : fdim (s.direction) = 2) {s₁ s₂ : euclidean_geometry.sphere P} {p₁ p₂ p : P} (hs₁ : s₁.center s) (hs₂ : s₂.center s) (hp₁s : p₁ s) (hp₂s : p₂ s) (hps : p s) (hs : s₁ s₂) (hp : p₁ p₂) (hp₁s₁ : p₁ s₁) (hp₂s₁ : p₂ s₁) (hps₁ : p s₁) (hp₁s₂ : p₁ s₂) (hp₂s₂ : p₂ s₂) (hps₂ : p s₂) :
p = p₁ p = p₂

Two spheres intersect in at most two points in a two-dimensional subspace containing their centers; this is a version of eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two for bundled spheres.

theorem euclidean_geometry.eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (hd : fdim V = 2) {s₁ s₂ : euclidean_geometry.sphere P} {p₁ p₂ p : P} (hs : s₁ s₂) (hp : p₁ p₂) (hp₁s₁ : p₁ s₁) (hp₂s₁ : p₂ s₁) (hps₁ : p s₁) (hp₁s₂ : p₁ s₂) (hp₂s₂ : p₂ s₂) (hps₂ : p s₂) :
p = p₁ p = p₂

Two spheres intersect in at most two points in two-dimensional space; this is a version of eq_of_dist_eq_of_dist_eq_of_finrank_eq_two for bundled spheres.

theorem euclidean_geometry.inner_pos_or_eq_of_dist_le_radius {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ : P} (hp₁ : p₁ s) (hp₂ : s.center s.radius) :
0 < has_inner.inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center) p₁ = p₂

Given a point on a sphere and a point not outside it, the inner product between the difference of those points and the radius vector is positive unless the points are equal.

theorem euclidean_geometry.inner_nonneg_of_dist_le_radius {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ : P} (hp₁ : p₁ s) (hp₂ : s.center s.radius) :
0 has_inner.inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)

Given a point on a sphere and a point not outside it, the inner product between the difference of those points and the radius vector is nonnegative.

theorem euclidean_geometry.inner_pos_of_dist_lt_radius {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ : P} (hp₁ : p₁ s) (hp₂ : s.center < s.radius) :
0 < has_inner.inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)

Given a point on a sphere and a point inside it, the inner product between the difference of those points and the radius vector is positive.

theorem euclidean_geometry.wbtw_of_collinear_of_dist_center_le_radius {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : {p₁, p₂, p₃}) (hp₁ : p₁ s) (hp₂ : s.center s.radius) (hp₃ : p₃ s) (hp₁p₃ : p₁ p₃) :
p₁ p₂ p₃

Given three collinear points, two on a sphere and one not outside it, the one not outside it is weakly between the other two points.

theorem euclidean_geometry.sbtw_of_collinear_of_dist_center_lt_radius {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p₁ p₂ p₃ : P} (h : {p₁, p₂, p₃}) (hp₁ : p₁ s) (hp₂ : s.center < s.radius) (hp₃ : p₃ s) (hp₁p₃ : p₁ p₃) :
p₁ p₂ p₃

Given three collinear points, two on a sphere and one inside it, the one inside it is strictly between the other two points.