# 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*][simon2011]

## TODO #

Define intrinsic frontier/interior and prove the lemmas related to exposed sets and points.

Generalise to Locally Convex Topological Vector Spacesβ’

More not-yet-PRed stuff is available on the branch `sperner_again`

.

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`

.

## Instances For

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

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

## Instances For

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.

## Instances For

Exposed points exactly correspond to exposed singletons.