Tangency for spheres.

This file defines notions of spheres being tangent to affine subspaces and other spheres.

Main definitions

• EuclideanGeometry.Sphere.orthRadius: the affine subspace orthogonal to the radius vector at a point (the tangent space, if that point lies in the sphere).

• EuclideanGeometry.Sphere.IsTangentAt: the property of an affine subspace being tangent to a sphere at a given point.

• EuclideanGeometry.Sphere.IsTangent: the property of an affine subspace being tangent to a sphere at some point.

• EuclideanGeometry.Sphere.tangentSet: the set of all maximal tangent spaces to a given sphere.

• EuclideanGeometry.Sphere.tangentsFrom: the set of all maximal tangent spaces to a given sphere and containing a given point.

• EuclideanGeometry.Sphere.commonTangents: the set of all maximal common tangent spaces to two given spheres.

• EuclideanGeometry.Sphere.commonIntTangents: the set of all maximal common internal tangent spaces to two given spheres.

• EuclideanGeometry.Sphere.commonExtTangents: the set of all maximal common external tangent spaces to two given spheres.

• EuclideanGeometry.Sphere.IsExtTangentAt: the property of two spheres being externally tangent at a given point.

• EuclideanGeometry.Sphere.IsIntTangentAt: the property of two spheres being internally tangent at a given point.

• EuclideanGeometry.Sphere.IsExtTangent: the property of two spheres being externally tangent.

• EuclideanGeometry.Sphere.IsIntTangent: the property of two spheres being internally tangent.

def EuclideanGeometry.Sphere.orthRadius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p : P) : AffineSubspace ℝ P

The affine subspace orthogonal to the radius vector of the sphere s at the point p (in the typical cases, p lies in s and this is the tangent space).

Equations

• s.orthRadius p = AffineSubspace.mk' p (Submodule.span ℝ {p -ᵥ s.center})ᗮ

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

theorem EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_left {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p x : P} : x ∈ s.orthRadius p ↔ inner (x -ᵥ p) (p -ᵥ s.center) = 0

theorem EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_right {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p x : P} : x ∈ s.orthRadius p ↔ inner (p -ᵥ s.center) (x -ᵥ p) = 0

@[simp]

theorem EuclideanGeometry.Sphere.direction_orthRadius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p : P) : (s.orthRadius p).direction = (Submodule.span ℝ {p -ᵥ s.center})ᗮ

@[simp]

theorem EuclideanGeometry.Sphere.orthRadius_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) : s.orthRadius s.center = ⊤

@[simp]

theorem EuclideanGeometry.Sphere.center_mem_orthRadius_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} : s.center ∈ s.orthRadius p ↔ p = s.center

theorem EuclideanGeometry.Sphere.orthRadius_le_orthRadius_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} : s.orthRadius p ≤ s.orthRadius q ↔ p = q ∨ q = s.center

@[simp]

theorem EuclideanGeometry.Sphere.orthRadius_eq_orthRadius_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} : s.orthRadius p = s.orthRadius q ↔ p = q

structure EuclideanGeometry.Sphere.IsTangentAt {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p : P) (as : AffineSubspace ℝ P) : Prop

The affine subspace as is tangent to the sphere s at the point p.

• mem_sphere : p ∈ s
• mem_space : p ∈ as
• le_orthRadius : as ≤ s.orthRadius p

@[simp]

theorem EuclideanGeometry.Sphere.isTangentAt_orthRadius_iff_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} : s.IsTangentAt p (s.orthRadius p) ↔ p ∈ s

theorem EuclideanGeometry.Sphere.IsTangentAt.inner_left_eq_zero_of_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} {as : AffineSubspace ℝ P} (h : s.IsTangentAt p as) {x : P} (hx : x ∈ as) : inner (x -ᵥ p) (p -ᵥ s.center) = 0

theorem EuclideanGeometry.Sphere.IsTangentAt.inner_right_eq_zero_of_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} {as : AffineSubspace ℝ P} (h : s.IsTangentAt p as) {x : P} (hx : x ∈ as) : inner (p -ᵥ s.center) (x -ᵥ p) = 0

theorem EuclideanGeometry.Sphere.IsTangentAt.eq_of_isTangentAt {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p q : P} {as : AffineSubspace ℝ P} (hp : s.IsTangentAt p as) (hq : s.IsTangentAt q as) : p = q

theorem EuclideanGeometry.Sphere.isTangentAt_center_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {as : AffineSubspace ℝ P} : s.IsTangentAt s.center as ↔ s.radius = 0 ∧ s.center ∈ as

def EuclideanGeometry.Sphere.IsTangent {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (as : AffineSubspace ℝ P) : Prop

The affine subspace as is tangent to the sphere s at some point.

Equations

• s.IsTangent as = ∃ (p : P), s.IsTangentAt p as

theorem EuclideanGeometry.Sphere.IsTangentAt.isTangent {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} {as : AffineSubspace ℝ P} (h : s.IsTangentAt p as) : s.IsTangent as

@[simp]

theorem EuclideanGeometry.Sphere.isTangent_orthRadius_iff_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} : s.IsTangent (s.orthRadius p) ↔ p ∈ s

def EuclideanGeometry.Sphere.tangentSet {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) : Set (AffineSubspace ℝ P)

The set of all maximal tangent spaces to the sphere s.

Equations

• s.tangentSet = s.orthRadius '' Metric.sphere s.center s.radius

theorem EuclideanGeometry.Sphere.mem_tangentSet_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s : Sphere P} : as ∈ s.tangentSet ↔ ∃ p ∈ s, s.orthRadius p = as

theorem EuclideanGeometry.Sphere.isTangent_of_mem_tangentSet {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s : Sphere P} (h : as ∈ s.tangentSet) : s.IsTangent as

def EuclideanGeometry.Sphere.tangentsFrom {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Sphere P) (p : P) : Set (AffineSubspace ℝ P)

The set of all maximal tangent spaces to the sphere s containing the point p.

Equations

• s.tangentsFrom p = {as : AffineSubspace ℝ P | as ∈ s.tangentSet ∧ p ∈ as}

theorem EuclideanGeometry.Sphere.mem_tangentsFrom_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s : Sphere P} {p : P} : as ∈ s.tangentsFrom p ↔ as ∈ s.tangentSet ∧ p ∈ as

theorem EuclideanGeometry.Sphere.mem_tangentSet_of_mem_tangentsFrom {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s : Sphere P} {p : P} (h : as ∈ s.tangentsFrom p) : as ∈ s.tangentSet

theorem EuclideanGeometry.Sphere.mem_of_mem_tangentsFrom {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s : Sphere P} {p : P} (h : as ∈ s.tangentsFrom p) : p ∈ as

theorem EuclideanGeometry.Sphere.isTangent_of_mem_tangentsFrom {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s : Sphere P} {p : P} (h : as ∈ s.tangentsFrom p) : s.IsTangent as

def EuclideanGeometry.Sphere.commonTangents {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s₁ s₂ : Sphere P) : Set (AffineSubspace ℝ P)

The set of all maximal common tangent spaces to the spheres s₁ and s₂.

Equations

• s₁.commonTangents s₂ = s₁.tangentSet ∩ s₂.tangentSet

theorem EuclideanGeometry.Sphere.mem_commonTangents_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s₁ s₂ : Sphere P} : as ∈ s₁.commonTangents s₂ ↔ as ∈ s₁.tangentSet ∧ as ∈ s₂.tangentSet

theorem EuclideanGeometry.Sphere.commonTangents_comm {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s₁ s₂ : Sphere P) : s₁.commonTangents s₂ = s₂.commonTangents s₁

def EuclideanGeometry.Sphere.commonIntTangents {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s₁ s₂ : Sphere P) : Set (AffineSubspace ℝ P)

The set of all maximal common internal tangent spaces to the spheres s₁ and s₂: tangent spaces containing a point weakly between the centers of the spheres.

Equations

• s₁.commonIntTangents s₂ = {as : AffineSubspace ℝ P | as ∈ s₁.commonTangents s₂ ∧ ∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center}

def EuclideanGeometry.Sphere.commonExtTangents {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s₁ s₂ : Sphere P) : Set (AffineSubspace ℝ P)

The set of all maximal common external tangent spaces to the spheres s₁ and s₂: tangent spaces not containing a point strictly between the centers of the spheres. (In the degenerate case where the two spheres are the same sphere with radius 0, the space is considered both an internal and an external common tangent.)

Equations

• s₁.commonExtTangents s₂ = {as : AffineSubspace ℝ P | as ∈ s₁.commonTangents s₂ ∧ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center}

theorem EuclideanGeometry.Sphere.mem_commonIntTangents_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s₁ s₂ : Sphere P} : as ∈ s₁.commonIntTangents s₂ ↔ as ∈ s₁.commonTangents s₂ ∧ ∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center

theorem EuclideanGeometry.Sphere.mem_commonExtTangents_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s₁ s₂ : Sphere P} : as ∈ s₁.commonExtTangents s₂ ↔ as ∈ s₁.commonTangents s₂ ∧ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center

@[simp]

theorem EuclideanGeometry.Sphere.commonIntTangents_union_commonExtTangents {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s₁ s₂ : Sphere P) : s₁.commonIntTangents s₂ ∪ s₁.commonExtTangents s₂ = s₁.commonTangents s₂

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

The spheres s₁ and s₂ are externally tangent at the point p.

• mem_left : p ∈ s₁
• mem_right : p ∈ s₂
• wbtw : Wbtw ℝ s₁.center p s₂.center

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

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

theorem EuclideanGeometry.Sphere.isExtTangentAt_center_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s₁ s₂ : Sphere P} : s₁.IsExtTangentAt s₂ s₁.center ↔ s₁.radius = 0 ∧ s₁.center ∈ s₂

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

The sphere s₁ is internally tangent to the sphere s₂ at the point p (that is, s₁ lies inside s₂ and is tangent to it at that point). This includes the degenerate case where the spheres are the same.

• mem_left : p ∈ s₁
• mem_right : p ∈ s₂
• wbtw : Wbtw ℝ s₂.center s₁.center p

theorem EuclideanGeometry.Sphere.isIntTangentAt_center_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s₁ s₂ : Sphere P} : s₁.IsIntTangentAt s₂ s₁.center ↔ s₁.radius = 0 ∧ s₁.center ∈ s₂

@[simp]

theorem EuclideanGeometry.Sphere.isIntTangentAt_self_iff_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p : P} : s.IsIntTangentAt s p ↔ p ∈ s

def EuclideanGeometry.Sphere.IsExtTangent {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s₁ s₂ : Sphere P) : Prop

The spheres s₁ and s₂ are externally tangent at some point.

Equations

• s₁.IsExtTangent s₂ = ∃ (p : P), s₁.IsExtTangentAt s₂ p

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

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

def EuclideanGeometry.Sphere.IsIntTangent {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s₁ s₂ : Sphere P) : Prop

The sphere s₁ is internally tangent to the sphere s₂ at some point.

Equations

• s₁.IsIntTangent s₂ = ∃ (p : P), s₁.IsIntTangentAt s₂ p

theorem EuclideanGeometry.Sphere.IsExtTangentAt.isExtTangent {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s₁ s₂ : Sphere P} {p : P} (h : s₁.IsExtTangentAt s₂ p) : s₁.IsExtTangent s₂

theorem EuclideanGeometry.Sphere.IsIntTangentAt.isIntTangent {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s₁ s₂ : Sphere P} {p : P} (h : s₁.IsIntTangentAt s₂ p) : s₁.IsIntTangent s₂

@[simp]

theorem EuclideanGeometry.Sphere.isIntTangent_self_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Nontrivial V] {s : Sphere P} : s.IsIntTangent s ↔ 0 ≤ s.radius

theorem EuclideanGeometry.Sphere.IsExtTangent.dist_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s₁ s₂ : Sphere P} (h : s₁.IsExtTangent s₂) : dist s₁.center s₂.center = s₁.radius + s₂.radius

theorem EuclideanGeometry.Sphere.IsIntTangent.dist_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s₁ s₂ : Sphere P} (h : s₁.IsIntTangent s₂) : dist s₁.center s₂.center = s₂.radius - s₁.radius

theorem EuclideanGeometry.Sphere.isExtTangent_iff_dist_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s₁ s₂ : Sphere P} : s₁.IsExtTangent s₂ ↔ dist s₁.center s₂.center = s₁.radius + s₂.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius

theorem EuclideanGeometry.Sphere.isIntTangent_iff_dist_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Nontrivial V] {s₁ s₂ : Sphere P} : s₁.IsIntTangent s₂ ↔ dist s₁.center s₂.center = s₂.radius - s₁.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius