Theorems · Theorem · convex and discrete geometry

Convexity.StdSimplex.convexCombPair_restrict_restrict_compl

∀ {I : Type u_6} {K : Type u_8} [inst : Semifield K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  (w : Convexity.StdSimplex K I) (s : Set I) (hs : ∃ x ∈ s, w.weights x ≠ 0) (hs' : ∃ x ∈ sᶜ, w.weights x ≠ 0)
  [inst_3 : DecidablePred fun x => x ∈ s],
  Convexity.convexCombPair ((Finsupp.filter (fun x => x ∈ s) w.weights).sum fun _x k => k)
      ((Finsupp.filter (fun x => x ∉ s) w.weights).sum fun _x k => k) ⋯ ⋯ ⋯ (w.restrict s hs) (w.restrict sᶜ hs') =
    w

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemifieldLinearOrderIsStrictOrderedRingDecidablePred