Mathlib Map

Theorems · Definition · convex and discrete geometry

Convexity.StdSimplex.weights

{R : Type u} →
  [inst : LE R] → [inst_1 : AddCommMonoid R] → [inst_2 : One R] → {M : Type v} → Convexity.StdSimplex R M → M →₀ R

The weights of the StdSimplex as a Finsupp.

Defined in
Mathlib.Geometry.Convex.ConvexSpace.Defs
Cited by
63 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
LEAddCommMonoidOne
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Convexity.StdSimplex.map · cited by 43StdSimplex.mapConvexity.IsConvexSet · cited by 35Convexity.IsConvexSetConvexity.StdSimplex.weights_map · cited by 18StdSimplex.weights_mapConvexity.StdSimplex.ext · cited by 14StdSimplex.extConvexity.iConvexComb_congr · cited by 10Convexity.iConvexComb_con…Convexity.iConvexComb_eq_sum · cited by 9Convexity.iConvexComb_eq_…Convexity.IsModuleConvexSpace.sConvexComb_eq_sum · cited by 7IsModuleConvexSpace.sConv…Convexity.StdSimplex.restrict · cited by 6StdSimplex.restrictConvexity.StdSimplex.weights_duple · cited by 6StdSimplex.weights_dupleConvexity.IsConvexSet.sConvexComb_mem · cited by 5IsConvexSet.sConvexComb_m…Convexity.dist_iConvexComb_le · cited by 5Convexity.dist_iConvexCom…Convexity.StdSimplex.total · cited by 5StdSimplex.totalConvexity.StdSimplex.weights_sConvexComb · cited by 5StdSimplex.weights_sConve…Convexity.StdSimplex.weights_single · cited by 5StdSimplex.weights_singleConvexity.StdSimplex.join · cited by 4StdSimplex.joinAddCommMonoid · cited by 12281AddCommMonoidFinsupp · cited by 5255FinsuppConvexity.StdSimplex · cited by 123Convexity.StdSimplexStdSimplex.weightsCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by71

Results whose statement or proof uses this declaration.