toExposed — Mathlib

English

The operation toExposed constructs from a linear functional l and a set A the exposed subset consisting of points in A that maximize l over A.

Русский

Операция toExposed строит экспонированное множество из A по линейному функционалу l: точку x в A назван максимумом l на A, если l(x) ≥ l(y) для всех y ∈ A.

LaTeX

$$$\\text{toExposed}(l,A) = \\{ x \\in A \\mid \\forall y \\in A,\\; l(y) \\le l(x) \\}.$$$

Lean4

/-- A useful way to build exposed sets from intersecting `A` with half-spaces (modelled by an
inequality with a functional). -/
def toExposed (l : StrongDual 𝕜 E) (A : Set E) : Set E :=
  {x ∈ A | ∀ y ∈ A, l y ≤ l x}

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