# mathlib3documentation

geometry.euclidean.sphere.second_inter

# Second intersection of a sphere and a line #

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 the second intersection of a sphere with a line through a point on that sphere.

## Main definitions #

• euclidean_geometry.sphere.second_inter is the second intersection of a sphere with a line through a point on that sphere.
noncomputable def euclidean_geometry.sphere.second_inter {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p : P) (v : V) :
P

The second intersection of a sphere with a line through a point on that sphere; that point if it is the only point of intersection of the line with the sphere. The intended use of this definition is when p ∈ s; the definition does not use s.radius, so in general it returns the second intersection with the sphere through p and with center s.center.

Equations
@[simp]
theorem euclidean_geometry.sphere.second_inter_dist {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p : P) (v : V) :

The distance between second_inter and the center equals the distance between the original point and the center.

@[simp]
theorem euclidean_geometry.sphere.second_inter_mem {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p : P} (v : V) :
s.second_inter p v s p s

The point given by second_inter lies on the sphere.

@[simp]
theorem euclidean_geometry.sphere.second_inter_zero (V : Type u_1) {P : Type u_2} [metric_space P] [ P] (p : P) :
s.second_inter p 0 = p

If the vector is zero, second_inter gives the original point.

theorem euclidean_geometry.sphere.second_inter_eq_self_iff {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p : P} {v : V} :
s.second_inter p v = p (p -ᵥ s.center) = 0

The point given by second_inter equals the original point if and only if the line is orthogonal to the radius vector.

theorem euclidean_geometry.sphere.eq_or_eq_second_inter_of_mem_mk'_span_singleton_iff_mem {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p : P} (hp : p s) {v : V} {p' : P} (hp' : p' (Span {v})) :
p' = p p' = s.second_inter p v p' s

A point on a line through a point on a sphere equals that point or second_inter.

@[simp]
theorem euclidean_geometry.sphere.second_inter_smul {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p : P) (v : V) {r : } (hr : r 0) :
s.second_inter p (r v) = s.second_inter p v

second_inter is unchanged by multiplying the vector by a nonzero real.

@[simp]
theorem euclidean_geometry.sphere.second_inter_neg {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p : P) (v : V) :

second_inter is unchanged by negating the vector.

@[simp]
theorem euclidean_geometry.sphere.second_inter_second_inter {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p : P) (v : V) :

Applying second_inter twice returns the original point.

theorem euclidean_geometry.sphere.second_inter_eq_line_map {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p p' : P) :
s.second_inter p (p' -ᵥ p) = p') ((-2) * has_inner.inner (p' -ᵥ p) (p -ᵥ s.center) / has_inner.inner (p' -ᵥ p) (p' -ᵥ p))

If the vector passed to second_inter is given by a subtraction involving the point in second_inter, the result of second_inter may be expressed using line_map.

theorem euclidean_geometry.sphere.second_inter_vsub_mem_affine_span {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p₁ p₂ : P) :
s.second_inter p₁ (p₂ -ᵥ p₁) {p₁, p₂}

If the vector passed to second_inter is given by a subtraction involving the point in second_inter, the result lies in the span of the two points.

theorem euclidean_geometry.sphere.second_inter_collinear {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p p' : P) :
{p, p', s.second_inter p (p' -ᵥ p)}

If the vector passed to second_inter is given by a subtraction involving the point in second_inter, the three points are collinear.

theorem euclidean_geometry.sphere.wbtw_second_inter {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p p' : P} (hp : p s) (hp' : s.center s.radius) :
p p' (s.second_inter p (p' -ᵥ p))

If the vector passed to second_inter is given by a subtraction involving the point in second_inter, and the second point is not outside the sphere, the second point is weakly between the first point and the result of second_inter.

theorem euclidean_geometry.sphere.sbtw_second_inter {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p p' : P} (hp : p s) (hp' : s.center < s.radius) :
p p' (s.second_inter p (p' -ᵥ p))

If the vector passed to second_inter is given by a subtraction involving the point in second_inter, and the second point is inside the sphere, the second point is strictly between the first point and the result of second_inter.