Theorems · Inductive type · convex and discrete geometry

Convexity.ConvexSpace

(R : Type u) →
  Type v → [inst₁ : PartialOrder R] → [inst₂ : Semiring R] → [inst₃ : IsStrictOrderedRing R] → Type (max u v)

A set equipped with an operation of finite convex combinations, where the coefficients must be non-negative and sum to 1.

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Defs

Cited by

176 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 4 definitions · uses no axioms

Assumes

PartialOrderSemiringIsStrictOrderedRing