# Exposed sets #

This file defines exposed sets and exposed points for sets in a real vector space.

An exposed subset of `A`

is a subset of `A`

that is the set of all maximal points of a functional
(a continuous linear map `E → 𝕜`

) over `A`

. By convention, `∅`

is an exposed subset of all sets.
This allows for better functoriality of the definition (the intersection of two exposed subsets is
exposed, faces of a polytope form a bounded lattice).
This is an analytic notion of "being on the side of". It is stronger than being extreme (see
`IsExposed.isExtreme`

), but weaker (for exposed points) than being a vertex.

An exposed set of `A`

is sometimes called a "face of `A`

", but we decided to reserve this
terminology to the more specific notion of a face of a polytope (sometimes hopefully soon out
on mathlib!).

## Main declarations #

`IsExposed 𝕜 A B`

: States that`B`

is an exposed set of`A`

(in the literature,`A`

is often implicit).`IsExposed.isExtreme`

: An exposed set is also extreme.

## References #

See chapter 8 of Barry Simon, *Convexity*

## TODO #

Prove lemmas relating exposed sets and points to the intrinsic frontier.

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`

.

## Equations

## Instances For

A useful way to build exposed sets from intersecting `A`

with halfspaces (modelled by an
inequality with a functional).

## Instances For

`IsExposed`

is *not* transitive: Consider a (topologically) open cube with vertices
`A₀₀₀, ..., A₁₁₁`

and add to it the triangle `A₀₀₀A₀₀₁A₀₁₀`

. Then `A₀₀₁A₀₁₀`

is an exposed subset
of `A₀₀₀A₀₀₁A₀₁₀`

which is an exposed subset of the cube, but `A₀₀₁A₀₁₀`

is not itself an exposed
subset of the cube.

If `B`

is a nonempty exposed subset of `A`

, then `B`

is the intersection of `A`

with some closed
halfspace. The converse is *not* true. It would require that the corresponding open halfspace
doesn't intersect `A`

.

For nontrivial `𝕜`

, if `B`

is an exposed subset of `A`

, then `B`

is the intersection of `A`

with
some closed halfspace. The converse is *not* true. It would require that the corresponding open
halfspace doesn't intersect `A`

.

A point is exposed with respect to `A`

iff there exists a hyperplane whose intersection with
`A`

is exactly that point.

## Equations

## Instances For

Exposed points exactly correspond to exposed singletons.