ConvexSpace

📁 Source: Mathlib/LinearAlgebra/ConvexSpace.lean

Statistics

Metric	Count
Definitions ConvexSpace, convexCombination, duple, join, map, single, weights, convexComboPair	8
Theorems assoc, single, ext, ext_iff, mk_single, nonneg, total, convexComboPair_one, convexComboPair_same, convexComboPair_zero	10
Total	18

ConvexSpace

Definitions

Name	Category	Theorems
convexCombination 📖	CompOp	2 math math: single, assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
assoc 📖	mathematical	—	convexCombination StdSimplex.map StdSimplex Preorder.toLE PartialOrder.toPreorder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne StdSimplex.join	—	—
single 📖	mathematical	—	convexCombination StdSimplex.single	—	—

StdSimplex

Definitions

Name	Category	Theorems
duple 📖	CompOp	—
join 📖	CompOp	1 math math: ConvexSpace.assoc
map 📖	CompOp	1 math math: ConvexSpace.assoc
single 📖	CompOp	2 math math: mk_single, ConvexSpace.single
weights 📖	CompOp	3 math math: ext_iff, nonneg, total

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	weights Preorder.toLE PartialOrder.toPreorder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	—
ext_iff 📖	mathematical	—	weights Preorder.toLE PartialOrder.toPreorder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ext
mk_single 📖	mathematical	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instLE Preorder.toLE PartialOrder.toPreorder Finsupp.instZero Finsupp.single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finsupp.sum	single	—	—
nonneg 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instLE Finsupp.instZero weights	—	—
total 📖	mathematical	—	Finsupp.sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid weights	—	—

(root)

Definitions

Name	Category	Theorems
ConvexSpace 📖	CompData	—
convexComboPair 📖	CompOp	3 math math: convexComboPair_one, convexComboPair_same, convexComboPair_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convexComboPair_one 📖	mathematical	—	convexComboPair AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	Finsupp.single_zero add_zero ConvexSpace.single
convexComboPair_same 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	convexComboPair	—	ConvexSpace.single
convexComboPair_zero 📖	mathematical	—	convexComboPair MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Finsupp.single_zero zero_add ConvexSpace.single

---

← Back to Index