Theorems · Theorem · geometry

EuclideanGeometry.Sphere.wbtw_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 → Wbtw ℝ 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 not outside the sphere, the second point is weakly between the first point and the result of secondInter.

Defined in

Mathlib.Geometry.Euclidean.Sphere.SecondInter

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor