Norm from a bounded symmetric convex neighbourhood (source code)

= Norm from a bounded symmetric convex neighbourhood
{title2=$p_U(x)=\inf\{t>0:x\in tU\}$}

Let $X$ be a real <Hausdorff> <topological vector space>, and let $U$ be a bounded, convex, open <neighbourhood> of zero with $U=-U$. Its <Minkowski functional>
$$
p_U(x)=\inf\{t>0:x\in tU\}
$$
is a <norm> and $U=\{x:p_U(x)<1\}$. Convexity and symmetry give a real <balanced set>, so the gauge is a <seminorm>. Openness gives the displayed unit-ball identity.

To prove definiteness, suppose $p_U(x)=0$. For any zero <neighbourhood> $V$, boundedness of $U$ gives $\varepsilon U\subseteq V$ for a sufficiently small $\varepsilon>0$. Since $x\in\varepsilon U$, it belongs to every zero <neighbourhood>. The <Hausdorff> property forces $x=0$. The same boundedness comparison shows that the <norm topology> agrees with the original topology.

For a complex <vector space>, require $U$ to be balanced under complex scalars; symmetry under minus one alone only supplies the real homogeneity. The argument is independent of finite dimension and requires no Euclidean inner or outer balls.<Functional Analysis by Peter Philip>[Theorems 1.37 and 1.41, Minkowski functionals and normability]{ref}