Theorems · Definition · convex and discrete geometry

IsExposed

(𝕜 : Type u_1) →
  {E : Type u_2} →
    [TopologicalSpace 𝕜] →
      [inst : Semiring 𝕜] →
        [Preorder 𝕜] → [inst_2 : AddCommMonoid E] → [TopologicalSpace E] → [Module 𝕜 E] → Set E → Set E → Prop

A set B is exposed with respect to A iff it maximizes some functional over A (and contains all points maximizing it). Written IsExposed 𝕜 A B.

Defined in

Mathlib.Analysis.Convex.Exposed

Cited by

19 results in Mathlib

Foundations

Depth 23 from the axioms · uses no axioms

Assumes

TopologicalSpaceSemiringPreorderAddCommMonoidTopologicalSpaceModule