Theorems · Theorem · convex and discrete geometry

convexHull_basis_eq_stdSimplex

∀ (R : Type u_1) (ι : Type u_2) [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : Fintype ι]
  [inst_4 : DecidableEq ι], (convexHull R) (Set.range fun i j => if i = j then 1 else 0) = stdSimplex R ι

stdSimplex 𝕜 ι is the convex hull of the canonical basis in ι → 𝕜.

Defined in

Mathlib.Analysis.Convex.StdSimplex

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingFintypeDecidableEq