absConvexHull — Mathlib

English

A basic equation relating the absConvexHull with a closure construction

Русский

Базовое равенство для absConvexHull и конструкции замыкания

LaTeX

$$Eq (absConvexHull 𝕜) (ClosureOperator.ofCompletePred (AbsConvex 𝕜) ⋯)$$

Lean4

/-- The absolute convex hull of a set `s` is the minimal absolute convex set that includes `s`. -/
@[simps! isClosed]
def absConvexHull : ClosureOperator (Set E) :=
  .ofCompletePred (AbsConvex 𝕜) fun _ ↦ .sInter

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