Theorems · Definition · convex and discrete geometry

Convexity.convexHull

(R : Type u_1) →
  {X : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsStrictOrderedRing R] → [Convexity.ConvexSpace R X] → ClosureOperator (Set X)

The convex hull of a set s is the minimal convex set that includes s.

Defined in

Mathlib.Geometry.Convex.Hull

Cited by

22 results in Mathlib

Foundations

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

Assumes

SemiringPartialOrderIsStrictOrderedRingConvexity.ConvexSpace