Spheres #

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

Main definitions #

EuclideanGeometry.Sphere bundles a center and a radius.
EuclideanGeometry.Sphere.IsDiameter is the property of two points being the two endpoints of a diameter of a sphere.
EuclideanGeometry.Sphere.ofDiameter constructs the sphere on a given diameter.
EuclideanGeometry.Cospherical is the property of a set of points being equidistant from some point.
EuclideanGeometry.Concyclic is the property of a set of points being cospherical and coplanar.

structure EuclideanGeometry.Sphere (P : Type u_2) [MetricSpace 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.

center : P
center of this sphere
radius : ℝ
radius of the sphere; not required to be positive

Instances For

source

theorem EuclideanGeometry.Sphere.ext {P : Type u_2} {inst✝ : MetricSpace P} {x y : Sphere P} (center : x.center = y.center) (radius : x.radius = y.radius) :

x = y

source

📐 coverage

theorem EuclideanGeometry.Sphere.ext_iff {P : Type u_2} {inst✝ : MetricSpace P} {x y : Sphere P} :

x = y ↔ x.center = y.center ∧ x.radius = y.radius

source

📐 coverage

instance EuclideanGeometry.instNonemptySphere {P : Type u_2} [MetricSpace P] [Nonempty P] :

Nonempty (Sphere P)

source

🔸 coverage

@[implicit_reducible]

instance EuclideanGeometry.instCoeSphereSet {P : Type u_2} [MetricSpace P] :

Coe (Sphere P) (Set P)

source

🔸 coverage

@[implicit_reducible]

instance EuclideanGeometry.instMembershipSphere {P : Type u_2} [MetricSpace P] :

Membership P (Sphere P)

source

📐 coverage

theorem EuclideanGeometry.Sphere.mk_center {P : Type u_2} [MetricSpace P] (c : P) (r : ℝ) :

{ center := c, radius := r }.center = c

source

📐 coverage

theorem EuclideanGeometry.Sphere.mk_radius {P : Type u_2} [MetricSpace P] (c : P) (r : ℝ) :

{ center := c, radius := r }.radius = r

source

📐 coverage

@[simp]

theorem EuclideanGeometry.Sphere.mk_center_radius {P : Type u_2} [MetricSpace P] (s : Sphere P) :

{ center := s.center, radius := s.radius } = s

source

📐 coverage

@[simp]

theorem EuclideanGeometry.Sphere.coe_mk {P : Type u_2} [MetricSpace P] (c : P) (r : ℝ) :

Metric.sphere { center := c, radius := r }.center { center := c, radius := r }.radius = Metric.sphere c r

source

📐 coverage

theorem EuclideanGeometry.Sphere.mem_coe {P : Type u_2} [MetricSpace P] {p : P} {s : Sphere P} :

p ∈ Metric.sphere s.center s.radius ↔ p ∈ s

source

📐 coverage

@[simp]

theorem EuclideanGeometry.Sphere.mem_coe' {P : Type u_2} [MetricSpace P] {p : P} {s : Sphere P} :

dist p s.center = s.radius ↔ p ∈ s

source

📐 coverage

theorem EuclideanGeometry.mem_sphere {P : Type u_2} [MetricSpace P] {p : P} {s : Sphere P} :

p ∈ s ↔ dist p s.center = s.radius

source

📐 coverage

theorem EuclideanGeometry.mem_sphere' {P : Type u_2} [MetricSpace P] {p : P} {s : Sphere P} :

p ∈ s ↔ dist s.center p = s.radius

source

📐 coverage

theorem EuclideanGeometry.subset_sphere {P : Type u_2} [MetricSpace P] {ps : Set P} {s : Sphere P} :

ps ⊆ Metric.sphere s.center s.radius ↔ ∀ p ∈ ps, p ∈ s

source

📐 coverage

theorem EuclideanGeometry.dist_of_mem_subset_sphere {P : Type u_2} [MetricSpace P] {p : P} {ps : Set P} {s : Sphere P} (hp : p ∈ ps) (hps : ps ⊆ Metric.sphere s.center s.radius) :

dist p s.center = s.radius

source

📐 coverage

theorem EuclideanGeometry.dist_of_mem_subset_mk_sphere {P : Type u_2} [MetricSpace P] {p c : P} {ps : Set P} {r : ℝ} (hp : p ∈ ps) (hps : ps ⊆ Metric.sphere { center := c, radius := r }.center { center := c, radius := r }.radius) :

dist p c = r

source

theorem EuclideanGeometry.Sphere.ne_iff {P : Type u_2} [MetricSpace P] {s₁ s₂ : Sphere P} :

s₁ ≠ s₂ ↔ s₁.center ≠ s₂.center ∨ s₁.radius ≠ s₂.radius

source

📐 coverage

theorem EuclideanGeometry.Sphere.center_eq_iff_eq_of_mem {P : Type u_2} [MetricSpace P] {s₁ s₂ : Sphere P} {p : P} (hs₁ : p ∈ s₁) (hs₂ : p ∈ s₂) :

s₁.center = s₂.center ↔ s₁ = s₂

source

theorem EuclideanGeometry.Sphere.center_ne_iff_ne_of_mem {P : Type u_2} [MetricSpace P] {s₁ s₂ : Sphere P} {p : P} (hs₁ : p ∈ s₁) (hs₂ : p ∈ s₂) :

s₁.center ≠ s₂.center ↔ s₁ ≠ s₂

source

📐 coverage

theorem EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere {P : Type u_2} [MetricSpace P] {p₁ p₂ : P} {s : Sphere P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) :

dist p₁ s.center = dist p₂ s.center

source

📐 coverage

theorem EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere' {P : Type u_2} [MetricSpace P] {p₁ p₂ : P} {s : Sphere P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) :

dist s.center p₁ = dist s.center p₂

source

📐 coverage

theorem EuclideanGeometry.Sphere.radius_nonneg_of_mem {P : Type u_2} [MetricSpace P] {s : Sphere P} {p : P} (h : p ∈ s) :

0 ≤ s.radius

source

📐 coverage

@[simp]

theorem EuclideanGeometry.Sphere.center_mem_iff {P : Type u_2} [MetricSpace P] {s : Sphere P} :

s.center ∈ s ↔ s.radius = 0

source

🔹 coverage

def EuclideanGeometry.Cospherical {P : Type u_2} [MetricSpace 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.

Instances For

source

📐 coverage

theorem EuclideanGeometry.cospherical_def {P : Type u_2} [MetricSpace P] (ps : Set P) :

Cospherical ps ↔ ∃ (center : P) (radius : ℝ), ∀ p ∈ ps, dist p center = radius

The definition of Cospherical.

source

📐 coverage

theorem EuclideanGeometry.cospherical_iff_exists_sphere {P : Type u_2} [MetricSpace P] {ps : Set P} :

Cospherical ps ↔ ∃ (s : Sphere P), ps ⊆ Metric.sphere s.center s.radius

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

source

📐 coverage

theorem EuclideanGeometry.Sphere.cospherical {P : Type u_2} [MetricSpace P] (s : Sphere P) :

Cospherical (Metric.sphere s.center s.radius)

The set of points in a sphere is cospherical.

source

📐 coverage

theorem EuclideanGeometry.Cospherical.subset {P : Type u_2} [MetricSpace P] {ps₁ ps₂ : Set P} (hs : ps₁ ⊆ ps₂) (hc : Cospherical ps₂) :

Cospherical ps₁

A subset of a cospherical set is cospherical.

source

📐 coverage

theorem EuclideanGeometry.cospherical_empty {P : Type u_2} [MetricSpace P] [Nonempty P] :

Cospherical ∅

The empty set is cospherical.

source

📐 coverage

theorem EuclideanGeometry.cospherical_singleton {P : Type u_2} [MetricSpace P] (p : P) :

Cospherical {p}

A single point is cospherical.

source

📐 coverage

theorem Isometry.cospherical {E : Type u_3} {F : Type u_4} [MetricSpace E] [MetricSpace F] {f : E → F} (hf : Isometry f) {ps : Set E} (hps : EuclideanGeometry.Cospherical ps) :

EuclideanGeometry.Cospherical (f '' ps)

If ps is cospherical, then any of its isometric images is cospherical.

source

📐 coverage

theorem EuclideanGeometry.Cospherical.inclusion {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {S₁ S₂ : AffineSubspace ℝ P} [Nonempty ↥S₁] {ps : Set ↥S₁} (hps : Cospherical ps) (hS : S₁ ≤ S₂) :

Cospherical (⇑(AffineSubspace.inclusion hS) '' ps)

If a set of points is cospherical, then its image under the inclusion of any affine subspace containing it is cospherical.

source

📐 coverage

theorem EuclideanGeometry.Cospherical.subtype_val {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {S : AffineSubspace ℝ P} [Nonempty ↥S] {ps : Set ↥S} (hps : Cospherical ps) :

Cospherical (Subtype.val '' ps)

If a set of points in an affine subspace is cospherical, then its image under the coercion to the ambient space is cospherical.

source

📐 coverage

theorem EuclideanGeometry.Sphere.nonempty_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Nontrivial V] {s : Sphere P} :

(Metric.sphere s.center s.radius).Nonempty ↔ 0 ≤ s.radius

source

📐 coverage

theorem EuclideanGeometry.cospherical_pair {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ : P) :

Cospherical {p₁, p₂}

Two points are cospherical.

source

🔶 coverage

structure EuclideanGeometry.Concyclic {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor 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.)

Cospherical : EuclideanGeometry.Cospherical ps
Coplanar : _root_.Coplanar ℝ ps

Instances For

source

📐 coverage

theorem EuclideanGeometry.Concyclic.subset {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {ps₁ ps₂ : Set P} (hs : ps₁ ⊆ ps₂) (h : Concyclic ps₂) :

Concyclic ps₁

A subset of a concyclic set is concyclic.

source

📐 coverage

theorem EuclideanGeometry.concyclic_empty {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] :

Concyclic ∅

The empty set is concyclic.

source

📐 coverage

theorem EuclideanGeometry.concyclic_singleton {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p : P) :

Concyclic {p}

A single point is concyclic.

source

📐 coverage

theorem EuclideanGeometry.concyclic_pair {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ : P) :

Concyclic {p₁, p₂}

Two points are concyclic.

source

🔶 coverage

structure EuclideanGeometry.Sphere.IsDiameter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p₁ p₂ : P) :

Prop

s.IsDiameter p₁ p₂ says that p₁ and p₂ are the two endpoints of a diameter of s.

left_mem : p₁ ∈ s
midpoint_eq_center : midpoint ℝ p₁ p₂ = s.center

Instances For

source

📐 coverage

theorem EuclideanGeometry.Sphere.IsDiameter.right_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} (h : s.IsDiameter p₁ p₂) :

p₂ ∈ s

source

📐 coverage

theorem EuclideanGeometry.Sphere.IsDiameter.symm {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} (h : s.IsDiameter p₁ p₂) :

s.IsDiameter p₂ p₁

source

📐 coverage

theorem EuclideanGeometry.Sphere.isDiameter_comm {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} :

s.IsDiameter p₁ p₂ ↔ s.IsDiameter p₂ p₁

source

📐 coverage

theorem EuclideanGeometry.Sphere.isDiameter_iff_left_mem_and_midpoint_eq_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} :

s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ midpoint ℝ p₁ p₂ = s.center

source

📐 coverage

theorem EuclideanGeometry.Sphere.isDiameter_iff_right_mem_and_midpoint_eq_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} :

s.IsDiameter p₁ p₂ ↔ p₂ ∈ s ∧ midpoint ℝ p₁ p₂ = s.center

source

📐 coverage

theorem EuclideanGeometry.Sphere.IsDiameter.pointReflection_center_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} (h : s.IsDiameter p₁ p₂) :

(Equiv.pointReflection s.center) p₁ = p₂

source

📐 coverage

theorem EuclideanGeometry.Sphere.IsDiameter.pointReflection_center_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} (h : s.IsDiameter p₁ p₂) :

(Equiv.pointReflection s.center) p₂ = p₁

source

📐 coverage

theorem EuclideanGeometry.Sphere.isDiameter_iff_left_mem_and_pointReflection_center_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} :

s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ (Equiv.pointReflection s.center) p₁ = p₂

source

📐 coverage

theorem EuclideanGeometry.Sphere.isDiameter_iff_right_mem_and_pointReflection_center_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} :

s.IsDiameter p₁ p₂ ↔ p₂ ∈ s ∧ (Equiv.pointReflection s.center) p₂ = p₁

source

theorem EuclideanGeometry.Sphere.IsDiameter.right_eq_of_isDiameter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ p₃ : P} (h₁₂ : s.IsDiameter p₁ p₂) (h₁₃ : s.IsDiameter p₁ p₃) :

p₂ = p₃

source

theorem EuclideanGeometry.Sphere.IsDiameter.left_eq_of_isDiameter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ p₃ : P} (h₁₃ : s.IsDiameter p₁ p₃) (h₂₃ : s.IsDiameter p₂ p₃) :

p₁ = p₂

source

📐 coverage

theorem EuclideanGeometry.Sphere.IsDiameter.dist_left_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} (h : s.IsDiameter p₁ p₂) :

dist p₁ p₂ = 2 * s.radius

source

📐 coverage

theorem EuclideanGeometry.Sphere.IsDiameter.dist_left_right_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} (h : s.IsDiameter p₁ p₂) :

dist p₁ p₂ / 2 = s.radius

source

📐 coverage

theorem EuclideanGeometry.Sphere.IsDiameter.left_eq_right_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} (h : s.IsDiameter p₁ p₂) :

p₁ = p₂ ↔ s.radius = 0

source

theorem EuclideanGeometry.Sphere.IsDiameter.left_ne_right_iff_radius_ne_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} (h : s.IsDiameter p₁ p₂) :

p₁ ≠ p₂ ↔ s.radius ≠ 0

source

📐 coverage

theorem EuclideanGeometry.Sphere.IsDiameter.left_ne_right_iff_radius_pos {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} (h : s.IsDiameter p₁ p₂) :

p₁ ≠ p₂ ↔ 0 < s.radius

source

📐 coverage

theorem EuclideanGeometry.Sphere.IsDiameter.wbtw {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} (h : s.IsDiameter p₁ p₂) :

Wbtw ℝ p₁ s.center p₂

source

📐 coverage

theorem EuclideanGeometry.Sphere.IsDiameter.sbtw {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} (h : s.IsDiameter p₁ p₂) (hr : s.radius ≠ 0) :

Sbtw ℝ p₁ s.center p₂

source

🔸 coverage

noncomputable def EuclideanGeometry.Sphere.ofDiameter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ : P) :

Sphere P

Construct the sphere with the given diameter.

Instances For

source

📐 coverage

theorem EuclideanGeometry.Sphere.isDiameter_ofDiameter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ : P) :

(Sphere.ofDiameter p₁ p₂).IsDiameter p₁ p₂

source

📐 coverage

theorem EuclideanGeometry.Sphere.IsDiameter.ofDiameter_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} (h : s.IsDiameter p₁ p₂) :

Sphere.ofDiameter p₁ p₂ = s

source

📐 coverage

theorem EuclideanGeometry.Sphere.isDiameter_iff_ofDiameter_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} :

s.IsDiameter p₁ p₂ ↔ Sphere.ofDiameter p₁ p₂ = s

source

📐 coverage

@[simp]

theorem EuclideanGeometry.Cospherical.subtype_val_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {S : AffineSubspace ℝ P} [Nonempty ↥S] [S.direction.HasOrthogonalProjection] {ps : Set ↥S} :

Cospherical (Subtype.val '' ps) ↔ Cospherical ps

A set of points in an affine subspace is cospherical if and only if its image in the ambient space is cospherical.

source

📐 coverage

theorem EuclideanGeometry.Cospherical.inclusion_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {S₁ S₂ : AffineSubspace ℝ P} [Nonempty ↥S₁] {ps : Set ↥S₁} [S₁.direction.HasOrthogonalProjection] [S₂.direction.HasOrthogonalProjection] (hS : S₁ ≤ S₂) :

Cospherical (⇑(AffineSubspace.inclusion hS) '' ps) ↔ Cospherical ps

A set of points is cospherical in an affine subspace S₁ if and only if its image under the inclusion into a larger affine subspace S₂ is cospherical.

source

📐 coverage

theorem EuclideanGeometry.Cospherical.affineIndependent {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Set P} (hs : Cospherical s) {p : Fin 3 → P} (hps : Set.range p ⊆ s) (hpi : Function.Injective p) :

AffineIndependent ℝ p

Any three points in a cospherical set are affinely independent.

source

📐 coverage

theorem EuclideanGeometry.Cospherical.affineIndependent_of_mem_of_ne {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Set P} (hs : Cospherical s) {p₁ p₂ p₃ : P} (h₁ : p₁ ∈ s) (h₂ : p₂ ∈ s) (h₃ : p₃ ∈ s) (h₁₂ : p₁ ≠ p₂) (h₁₃ : p₁ ≠ p₃) (h₂₃ : p₂ ≠ p₃) :

AffineIndependent ℝ ![p₁, p₂, p₃]

Any three points in a cospherical set are affinely independent.

source

📐 coverage

theorem EuclideanGeometry.Cospherical.affineIndependent_of_ne {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (hs : Cospherical {p₁, p₂, p₃}) (h₁₂ : p₁ ≠ p₂) (h₁₃ : p₁ ≠ p₃) (h₂₃ : p₂ ≠ p₃) :

AffineIndependent ℝ ![p₁, p₂, p₃]

The three points of a cospherical set are affinely independent.

source

📐 coverage

theorem EuclideanGeometry.inner_vsub_vsub_of_mem_sphere_of_mem_sphere {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ : P} {s₁ s₂ : Sphere P} (hp₁s₁ : p₁ ∈ s₁) (hp₂s₁ : p₂ ∈ s₁) (hp₁s₂ : p₁ ∈ s₂) (hp₂s₂ : p₂ ∈ s₂) :

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

📐 coverage

theorem EuclideanGeometry.Sphere.inner_vsub_center_midpoint_vsub {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ : P} {s : Sphere P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) :

inner ℝ (s.center -ᵥ midpoint ℝ p₁ p₂) (p₂ -ᵥ p₁) = 0

The vector from the midpoint of a chord to the center of the sphere is orthogonal to the chord.

source

📐 coverage

theorem EuclideanGeometry.Sphere.dist_center_lt_radius_of_sbtw {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p : P} {s : Sphere P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp : Sbtw ℝ p₁ p p₂) :

dist s.center p < s.radius

The distance from the center of a sphere to any point strictly between two points on the sphere is strictly less than the radius.

source

📐 coverage

theorem EuclideanGeometry.Sphere.dist_center_midpoint_lt_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ : P} {s : Sphere P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₁p₂ : p₁ ≠ p₂) :

dist s.center (midpoint ℝ p₁ p₂) < s.radius

The distance from the center of a sphere to the midpoint of a chord with distinct endpoints is strictly less than the radius.

source

theorem EuclideanGeometry.eq_of_mem_sphere_of_mem_sphere_of_mem_of_finrank_eq_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} [FiniteDimensional ℝ ↥s.direction] (hd : Module.finrank ℝ ↥s.direction = 2) {s₁ s₂ : 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 EuclideanGeometry.eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [FiniteDimensional ℝ V] (hd : Module.finrank ℝ V = 2) {s₁ s₂ : 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

📐 coverage

theorem EuclideanGeometry.inner_pos_or_eq_of_dist_le_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : dist p₂ s.center ≤ s.radius) :

0 < 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

📐 coverage

theorem EuclideanGeometry.inner_nonneg_of_dist_le_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : dist p₂ s.center ≤ s.radius) :

0 ≤ 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

📐 coverage

theorem EuclideanGeometry.inner_pos_of_dist_lt_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : dist p₂ s.center < s.radius) :

0 < 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

📐 coverage

theorem EuclideanGeometry.inner_vsub_center_vsub_pos {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ : P} {s : Sphere P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₁p₂ : p₁ ≠ p₂) :

0 < inner ℝ (p₂ -ᵥ p₁) (s.center -ᵥ p₁)

Given two distinct points on a sphere, the inner product of the chord with the radius vector at one endpoint is negative.

source

📐 coverage

theorem EuclideanGeometry.wbtw_of_collinear_of_dist_center_le_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ p₃ : P} (h : Collinear ℝ {p₁, p₂, p₃}) (hp₁ : p₁ ∈ s) (hp₂ : 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

📐 coverage

theorem EuclideanGeometry.sbtw_of_collinear_of_dist_center_lt_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ p₃ : P} (h : Collinear ℝ {p₁, p₂, p₃}) (hp₁ : p₁ ∈ s) (hp₂ : 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.

source

📐 coverage

theorem EuclideanGeometry.Sphere.isDiameter_iff_mem_and_mem_and_dist {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} :

s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius

source

📐 coverage

theorem EuclideanGeometry.Sphere.isDiameter_iff_mem_and_mem_and_wbtw {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ : P} :

s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂

Documentation

Mathlib.Geometry.Euclidean.Sphere.Basic

Spheres #

Main definitions #