Theorems · Theorem · geometry

EuclideanGeometry.Sphere.sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite

∀ {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} {n : ℕ} [inst_4 : NeZero n]
  {sx : Affine.Simplex ℝ P n} {i : Fin (n + 1)},
  sx.points i ∈ s →
    (∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius) →
      ∀ {p : P},
        p ∈ (sx.faceOpposite i).interior →
          (affineSpan ℝ (Set.range (sx.faceOpposite i).points)).SOppSide (sx.points i)
            (s.secondInter (sx.points i) (p -ᵥ sx.points i))

If the point passed to secondInter is a vertex of a simplex, lying on the sphere, and all vertices lie on or inside the sphere, and the vector passed to secondInter is given by a subtraction involving that vertex and a point in the interior of the opposite face, the given vertex and the result of secondInter are on opposite sides of that face.

Defined in

Mathlib.Geometry.Euclidean.Sphere.SecondInter

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorNeZero