mathlib3 documentation

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 #

source
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
source
theorem euclidean_geometry.sphere.ext_iff {P : Type u_2} {_inst_1 : metric_space P} (x y : euclidean_geometry.sphere P) :
x = y ↔ x.center = y.center ∧ x.radius = y.radius
source
@[ext]
structure euclidean_geometry.sphere (P : Type u_2) [metric_space P] :
Type u_2
  • center : P
  • radius : ℝ

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
source
@[protected, instance]
def euclidean_geometry.sphere.nonempty {P : Type u_2} [metric_space P] [nonempty P] :
nonempty (euclidean_geometry.sphere P)
source
@[protected, instance]
def euclidean_geometry.set.has_coe {P : Type u_2} [metric_space P] :
has_coe (euclidean_geometry.sphere P) (set P)
Equations
source
@[protected, instance]
def euclidean_geometry.sphere.has_mem {P : Type u_2} [metric_space P] :
has_mem P (euclidean_geometry.sphere P)
Equations
source
theorem euclidean_geometry.sphere.mk_center {P : Type u_2} [metric_space P] (c : P) (r : ℝ) :
{center := c, radius := r}.center = c
source
theorem euclidean_geometry.sphere.mk_radius {P : Type u_2} [metric_space P] (c : P) (r : ℝ) :
{center := c, radius := r}.radius = r
source
@[simp]
theorem euclidean_geometry.sphere.mk_center_radius {P : Type u_2} [metric_space P] (s : euclidean_geometry.sphere P) :
{center := s.center, radius := s.radius} = s
source
theorem euclidean_geometry.sphere.coe_def {P : Type u_2} [metric_space P] (s : euclidean_geometry.sphere P) :
↑s = metric.sphere s.center s.radius
source
@[simp]
theorem euclidean_geometry.sphere.coe_mk {P : Type u_2} [metric_space P] (c : P) (r : ℝ) :
↑{center := c, radius := r} = metric.sphere c r
source
@[simp]
theorem euclidean_geometry.sphere.mem_coe {P : Type u_2} [metric_space P] {p : P} {s : euclidean_geometry.sphere P} :
p ∈ ↑s ↔ p ∈ s
source
theorem euclidean_geometry.mem_sphere {P : Type u_2} [metric_space P] {p : P} {s : euclidean_geometry.sphere P} :
p ∈ s ↔ has_dist.dist p s.center = s.radius
source
theorem euclidean_geometry.mem_sphere' {P : Type u_2} [metric_space P] {p : P} {s : euclidean_geometry.sphere P} :
p ∈ s ↔ has_dist.dist s.center p = s.radius
source
theorem euclidean_geometry.subset_sphere {P : Type u_2} [metric_space P] {ps : set P} {s : euclidean_geometry.sphere P} :
ps ⊆ ↑s ↔ ∀ (p : P), p ∈ ps → p ∈ s
source
theorem euclidean_geometry.dist_of_mem_subset_sphere {P : Type u_2} [metric_space P] {p : P} {ps : set P} {s : euclidean_geometry.sphere P} (hp : p ∈ ps) (hps : ps ⊆ ↑s) :
has_dist.dist p s.center = s.radius
source
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}) :
has_dist.dist p c = r
source
theorem euclidean_geometry.sphere.ne_iff {P : Type u_2} [metric_space P] {s₁ s₂ : euclidean_geometry.sphere P} :
s₁ ≠ s₂ ↔ s₁.center ≠ s₂.center ∨ s₁.radius ≠ s₂.radius
source
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₂
source
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₂
source
theorem euclidean_geometry.dist_center_eq_dist_center_of_mem_sphere {P : Type u_2} [metric_space P] {p₁ p₂ : P} {s : euclidean_geometry.sphere P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) :
has_dist.dist p₁ s.center = has_dist.dist p₂ s.center
source
theorem euclidean_geometry.dist_center_eq_dist_center_of_mem_sphere' {P : Type u_2} [metric_space P] {p₁ p₂ : P} {s : euclidean_geometry.sphere P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) :
has_dist.dist s.center p₁ = has_dist.dist s.center p₂
source
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
source
theorem euclidean_geometry.cospherical_def {P : Type u_2} [metric_space P] (ps : set P) :
euclidean_geometry.cospherical ps ↔ ∃ (center : P) (radius : ℝ), ∀ (p : P), p ∈ ps → has_dist.dist p center = radius

The definition of cospherical.

source
theorem euclidean_geometry.cospherical_iff_exists_sphere {P : Type u_2} [metric_space P] {ps : set P} :
euclidean_geometry.cospherical ps ↔ ∃ (s : euclidean_geometry.sphere P), ps ⊆ ↑s

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

source
theorem euclidean_geometry.sphere.cospherical {P : Type u_2} [metric_space P] (s : euclidean_geometry.sphere P) :
euclidean_geometry.cospherical ↑s

The set of points in a sphere is cospherical.

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

A subset of a cospherical set is cospherical.

source
theorem euclidean_geometry.cospherical_empty {P : Type u_2} [metric_space P] [nonempty P] :
euclidean_geometry.cospherical ∅

The empty set is cospherical.

source
theorem euclidean_geometry.cospherical_singleton {P : Type u_2} [metric_space P] (p : P) :
euclidean_geometry.cospherical {p}

A single point is cospherical.

source
theorem euclidean_geometry.cospherical_pair {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [normed_space ℝ V] [metric_space P] [normed_add_torsor V P] (p₁ p₂ : P) :
euclidean_geometry.cospherical {p₁, p₂}

Two points are cospherical.

source
structure euclidean_geometry.concyclic {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [normed_space ℝ V] [metric_space P] [normed_add_torsor V P] (ps : set P) :
Prop

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.)

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

A subset of a concyclic set is concyclic.

source
theorem euclidean_geometry.concyclic_empty {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [normed_space ℝ V] [metric_space P] [normed_add_torsor V P] :
euclidean_geometry.concyclic ∅

The empty set is concyclic.

source
theorem euclidean_geometry.concyclic_singleton {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [normed_space ℝ V] [metric_space P] [normed_add_torsor V P] (p : P) :
euclidean_geometry.concyclic {p}

A single point is concyclic.

source
theorem euclidean_geometry.concyclic_pair {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [normed_space ℝ V] [metric_space P] [normed_add_torsor V P] (p₁ p₂ : P) :
euclidean_geometry.concyclic {p₁, p₂}

Two points are concyclic.

source
theorem euclidean_geometry.cospherical.affine_independent {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : set P} (hs : euclidean_geometry.cospherical s) {p : fin 3 → P} (hps : set.range p ⊆ s) (hpi : function.injective p) :
affine_independent ℝ p

Any three points in a cospherical set are affinely independent.

source
theorem euclidean_geometry.cospherical.affine_independent_of_mem_of_ne {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : set P} (hs : euclidean_geometry.cospherical s) {p₁ p₂ p₃ : P} (h₁ : p₁ ∈ s) (h₂ : p₂ ∈ s) (h₃ : p₃ ∈ s) (h₁₂ : p₁ ≠ p₂) (h₁₃ : p₁ ≠ p₃) (h₂₃ : p₂ ≠ p₃) :
affine_independent ℝ ![p₁, p₂, p₃]

Any three points in a cospherical set are affinely independent.

source
theorem euclidean_geometry.cospherical.affine_independent_of_ne {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p₁ p₂ p₃ : P} (hs : euclidean_geometry.cospherical {p₁, p₂, p₃}) (h₁₂ : p₁ ≠ p₂) (h₁₃ : p₁ ≠ p₃) (h₂₃ : p₂ ≠ p₃) :
affine_independent ℝ ![p₁, p₂, p₃]

The three points of a cospherical set are affinely independent.

source
theorem euclidean_geometry.inner_vsub_vsub_of_mem_sphere_of_mem_sphere {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V 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.)

source
theorem euclidean_geometry.eq_of_mem_sphere_of_mem_sphere_of_mem_of_finrank_eq_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [finite_dimensional ℝ ↥(s.direction)] (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.

source
theorem euclidean_geometry.eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [finite_dimensional ℝ V] (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.

source
theorem euclidean_geometry.inner_pos_or_eq_of_dist_le_radius {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : euclidean_geometry.sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : has_dist.dist p₂ 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.

source
theorem euclidean_geometry.inner_nonneg_of_dist_le_radius {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : euclidean_geometry.sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : has_dist.dist p₂ 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.

source
theorem euclidean_geometry.inner_pos_of_dist_lt_radius {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : euclidean_geometry.sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : has_dist.dist p₂ 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.

source
theorem euclidean_geometry.wbtw_of_collinear_of_dist_center_le_radius {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : euclidean_geometry.sphere P} {p₁ p₂ p₃ : P} (h : collinear ℝ {p₁, p₂, p₃}) (hp₁ : p₁ ∈ s) (hp₂ : has_dist.dist p₂ s.center ≤ s.radius) (hp₃ : p₃ ∈ s) (hp₁p₃ : p₁ ≠ p₃) :
wbtw ℝ 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.

source
theorem euclidean_geometry.sbtw_of_collinear_of_dist_center_lt_radius {V : Type u_1} {P : Type u_2} [normed_add_comm_group V] [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : euclidean_geometry.sphere P} {p₁ p₂ p₃ : P} (h : collinear ℝ {p₁, p₂, p₃}) (hp₁ : p₁ ∈ s) (hp₂ : has_dist.dist p₂ s.center < s.radius) (hp₃ : p₃ ∈ s) (hp₁p₃ : p₁ ≠ p₃) :
sbtw ℝ 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.