Convex hull #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines the convex hull of a set
s in a module.
convex_hull 𝕜 s is the smallest convex
s. In order theory speak, this is a closure operator.
Implementation notes #
convex_hull is defined as a closure operator. This gives access to the
while the impact on writing code is minimal as
convex_hull 𝕜 s is automatically elaborated as
⇑(convex_hull 𝕜) s.
The convex hull of a set
s is the minimal convex set that includes