Theorems · Definition · convex and discrete geometry

Convexity.IsConvexSet

(R : Type u_3) →
  {X : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : IsStrictOrderedRing R] → [Convexity.ConvexSpace R X] → Set X → Prop

A set s in a convex space is convex if all convex combinations of points in s lie themselves in s. When the scalars form a field, this is equivalent to the definition in terms of binary combinations. See IsConvexSet.of_convexCombPair_mem.

Defined in

Mathlib.Geometry.Convex.Set

Cited by

35 results in Mathlib

Foundations

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

Assumes

SemiringPartialOrderIsStrictOrderedRingConvexity.ConvexSpace