convexHull — Mathlib

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

Похожие утверждения