Theorems · Theorem · convex and discrete geometry

Convexity.ConvexSpace.convexCombination_single

Deprecated since 2026-05-04Use Convexity.ConvexSpace.sConvexComb_single instead.

∀ {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

Alias of Convexity.ConvexSpace.sConvexComb_single. A convex combination of a single point is that point.

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

Convexity.ConvexSpace