English
A point x is exposed with respect to A if there exists a linear functional ℓ that attains its maximum on A at x and is unique there.
Русский
Точка x экспонирована для A, если существует линейный функционал ℓ, достигающий максимума на A в точке x и достигающий его единожды.
LaTeX
$$$$ x \in A.exposedPoints 𝕜 \iff x \in A \wedge \exists \ell \in StrongDual 𝕜 E, \forall y \in A, \ell y \le \ell x \wedge (\ell x \le \ell y \rightarrow y = x). $$$$
Lean4
/-- A point is exposed with respect to `A` iff there exists a hyperplane whose intersection with
`A` is exactly that point. -/
def exposedPoints (A : Set E) : Set E :=
{x ∈ A | ∃ l : StrongDual 𝕜 E, ∀ y ∈ A, l y ≤ l x ∧ (l x ≤ l y → y = x)}
