English
The convex hull of a set s is the minimal convex set containing s.
Русский
Выпуклая оболочка множества s — это минимальное выпуклое множество, содержащее s.
LaTeX
$$$\\text{convexHull}_{\\mathbb{K}}(s) = \\bigcap_{t \\supseteq s,\\; \\mathrm{Convex}} t$$$
Lean4
/-- The convex hull of a set `s` is the minimal convex set that includes `s`. -/
@[simps! isClosed]
def convexHull : ClosureOperator (Set E) :=
.ofCompletePred (Convex 𝕜) fun _ ↦ convex_sInter