Theorems · Theorem · geometry

EuclideanGeometry.Sphere.sbtw_secondInter

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p p' : P},
  p ∈ s → dist p' s.center < s.radius → Sbtw ℝ p p' (s.secondInter p (p' -ᵥ p))

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

Defined in

Mathlib.Geometry.Euclidean.Sphere.SecondInter

Cited by

1 results in Mathlib

Foundations

Depth 177 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor