Theorems · Theorem · convex and discrete geometry

Convexity.StdSimplex.weights_restrict

∀ {X : Type u_2} {K : Type u_8} [inst : Semifield K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  (w : Convexity.StdSimplex K X) (s : Set X) (hs : ∃ x ∈ s, w.weights x ≠ 0) [inst_3 : DecidablePred fun x => x ∈ s],
  (w.restrict s hs).weights =
    ((Finsupp.filter (fun x => x ∈ s) w.weights).sum fun _x k => k)⁻¹ • Finsupp.filter (fun x => x ∈ s) w.weights

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemifieldLinearOrderIsStrictOrderedRingDecidablePred