Theorems · Theorem · convex and discrete geometry

Convexity.StdSimplex.restrict_singleton

∀ {X : Type u_2} {K : Type u_8} [inst : Semifield K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  [IsDomain K] (w : Convexity.StdSimplex K X) (x : X) (hx : ∃ x_1 ∈ {x}, w.weights x_1 ≠ 0),
  w.restrict {x} hx = Convexity.StdSimplex.single x

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemifieldLinearOrderIsStrictOrderedRingIsDomain