Theorems · Theorem · convex and discrete geometry

Convexity.StdSimplex.support_weights_restrict

∀ {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) (s : Set X) (hs : ∃ x ∈ s, w.weights x ≠ 0)
  [inst_4 : DecidablePred fun x => x ∈ s], (w.restrict s hs).weights.support = {x ∈ w.weights.support | x ∈ s}

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemifieldLinearOrderIsStrictOrderedRingIsDomainDecidablePred