Theorems · Theorem · convex and discrete geometry

Convexity.ConvexSpace.sConvexComb_single

∀ {R : Type u} {M : Type v} {inst₁ : PartialOrder R} {inst₂ : Semiring R} {inst₃ : IsStrictOrderedRing R}
  [self : Convexity.ConvexSpace R M] (x : M), Convexity.sConvexComb (Convexity.StdSimplex.single x) = x

A convex combination of a single point is that point.

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Defs

Cited by

9 results in Mathlib

Foundations

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

Assumes

Convexity.ConvexSpace