closedConvexHull — Mathlib

English

The closed convex hull of a set s is the smallest closed convex set that contains s.

Русский

Замкнутая выпуклая оболочка множества s — наименьшее замкнутое выпуклое множество, содержащее s.

LaTeX

$$$\text{closedConvexHull}_{\mathbb{K}}(s) = \bigcap\{t\subset E : \text{Convex}_{\mathbb{K}}(t) \wedge \text{IsClosed}(t) \wedge s \subseteq t\}$$$

Lean4

/-- The convex closed hull of a set `s` is the minimal convex closed set that includes `s`. -/
@[simps! isClosed]
def closedConvexHull : ClosureOperator (Set E) :=
  .ofCompletePred (fun s => Convex 𝕜 s ∧ IsClosed s) fun _ ↦ convex_closed_sInter

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