Bipolar theorem for a dual pair (source code)

= Bipolar theorem for a dual pair
{c}

For $A\subseteq E$ in a <dual pair> $(E,F)$, define $A^\circ=\{f\in F:f(a)\leq1\text{ for all }a\in A\}$. Then
$$
A^{\circ\circ}=\overline{\operatorname{conv}}^{\sigma(E,F)}(A\cup\{0\}).
$$