Theorems · Definition · functional analysis

closedAbsConvexHull

(𝕜 : Type u_1) →
  {E : Type u_2} →
    [SeminormedRing 𝕜] →
      [SMul 𝕜 E] → [AddCommMonoid E] → [PartialOrder 𝕜] → [TopologicalSpace E] → ClosureOperator (Set E)

The absolutely convex closed hull of a set s is the minimal absolutely convex closed set that includes s.

Defined in

Mathlib.Analysis.LocallyConvex.AbsConvex

Cited by

10 results in Mathlib

Foundations

Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedRingSMulAddCommMonoidPartialOrderTopologicalSpace