mathlib3 documentation

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 #

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]

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

@[simp]

The point given by second_inter lies on the sphere.

@[simp]

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

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

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} [normed_add_comm_group V] [inner_product_space V] [metric_space P] [normed_add_torsor V P] (s : euclidean_geometry.sphere 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]

second_inter is unchanged by negating the vector.

@[simp]

Applying second_inter twice returns the original point.

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.

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.

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

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.

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.