Theorems · Definition · convex and discrete geometry

Convexity.StdSimplex.restrict

{X : Type u_2} →
  {K : Type u_8} →
    [inst : Semifield K] →
      [inst_1 : LinearOrder K] →
        [IsStrictOrderedRing K] →
          (w : Convexity.StdSimplex K X) → (s : Set X) → (∃ x ∈ s, w.weights x ≠ 0) → Convexity.StdSimplex K X

Project an element of the standard simplex to a lower-dimensional standard simplex, assuming at least one non-zero weight subsists.

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Defs

Cited by

6 results in Mathlib

Foundations

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

Assumes

SemifieldLinearOrderIsStrictOrderedRing