Documentation

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

Instances For

@[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

theorem EuclideanGeometry.Sphere.IsTangentAt.dist_sq_eq_of_mem {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} (h : s.IsTangentAt p as) (hq : q ∈ as) :

dist q s.center ^ 2 = s.radius ^ 2 + dist q p ^ 2

theorem EuclideanGeometry.Sphere.IsTangentAt.mem_and_mem_iff_eq {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} (h : s.IsTangentAt p as) :

q ∈ s ∧ q ∈ as ↔ q = p

theorem EuclideanGeometry.Sphere.IsTangentAt.eq_of_mem_of_mem {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} (h : s.IsTangentAt p as) (hs : q ∈ s) (has : q ∈ as) :

q = p

theorem EuclideanGeometry.Sphere.IsTangentAt.dist_eq_of_mem_of_mem {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {p₁ p₂ q : P} {as₁ as₂ : AffineSubspace ℝ P} (h₁ : s.IsTangentAt p₁ as₁) (h₂ : s.IsTangentAt p₂ as₂) (hq_mem₁ : q ∈ as₁) (hq_mem₂ : q ∈ as₂) :

dist q p₁ = dist q p₂

If two tangent lines to a sphere pass through the same point q, then the distances from q to the tangent points are equal.

theorem EuclideanGeometry.Sphere.IsTangentAt.radius_lt_dist_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {as : AffineSubspace ℝ P} {p q : P} (h : s.IsTangentAt p as) (hq : q ∈ as) (hqp : q ≠ p) :

s.radius < dist q s.center

theorem EuclideanGeometry.Sphere.IsTangentAt.eq_orthRadius_of_finrank_add_one_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {as : AffineSubspace ℝ P} {p : P} (ht : s.IsTangentAt p as) (hr : s.radius ≠ 0) (hfr : Module.finrank ℝ ↥as.direction + 1 = Module.finrank ℝ V) :

as = s.orthRadius p

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

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

Equations

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

Instances For

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

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

s.radius ≤ dist p s.center

theorem EuclideanGeometry.Sphere.IsTangent.notMem_of_dist_lt {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {as : AffineSubspace ℝ P} (h : s.IsTangent as) {p : P} (hp : dist p s.center < s.radius) :

p ∉ as

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

Metric.infDist s.center ↑as = s.radius

theorem EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {as : AffineSubspace ℝ P} [Nonempty ↥as] [as.direction.HasOrthogonalProjection] :

dist s.center ↑((orthogonalProjection as) s.center) = s.radius ↔ s.IsTangentAt (↑((orthogonalProjection as) s.center)) as

theorem EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangent {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {as : AffineSubspace ℝ P} [Nonempty ↥as] [as.direction.HasOrthogonalProjection] :

dist s.center ↑((orthogonalProjection as) s.center) = s.radius ↔ s.IsTangent as

theorem EuclideanGeometry.Sphere.infDist_eq_radius_iff_isTangent {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {as : AffineSubspace ℝ P} [Nonempty ↥as] [as.direction.HasOrthogonalProjection] :

Metric.infDist s.center ↑as = s.radius ↔ s.IsTangent as

theorem EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {as : AffineSubspace ℝ P} [Nonempty ↥as] [as.direction.HasOrthogonalProjection] :

s.IsTangent as ↔ s.IsTangentAt (↑((orthogonalProjection as) s.center)) as

theorem EuclideanGeometry.Sphere.IsTangent.isTangentAt {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Sphere P} {as : AffineSubspace ℝ P} [Nonempty ↥as] [as.direction.HasOrthogonalProjection] :

s.IsTangent as → s.IsTangentAt (↑((orthogonalProjection as) s.center)) as

Alias of the forward direction of EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection.

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

as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center) p)

theorem EuclideanGeometry.Sphere.IsTangentAt.eq_orthogonalProjection {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} [Nonempty ↥as] [as.direction.HasOrthogonalProjection] (h : s.IsTangentAt p as) :

p = ↑((orthogonalProjection as) s.center)

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

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

Equations

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

Instances For

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

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}

Instances For

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

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

Equations

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

Instances For

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

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}

Instances For

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

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}

Instances For

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

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

Instances For

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