Convex hull #
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
Alias of the reverse direction of convex_hull_nonempty_iff`.