Minkowski gauge for an open convex zero-neighborhood

Let $X$ be a real or complex TVS (Topological vector spaces over the real and complex fields) and let $U$ be an open convex zero-neighborhood, with convexity as in Local convexity, convex and balanced sets, and the continuous dual. The Minkowski gauge of $U$ is $p_U:X⟶[0,\mathrm{\infty }),p_U(x)=\inf \{t>0:x\in tU\}\mathrm{.}$

This is a well-defined finite real number for each $x$. Indeed, Translations, dilations and absorption in a topological vector space gives $x\in tU$ for every sufficiently large positive real $t$, so the defining set is nonempty; zero is a lower bound. The infimum therefore exists in $\mathbb{R}$ by Every nonempty set bounded below has an infimum and is unique by the infimum convention of Greatest lower bound (infimum). It is nonnegative, since zero is a lower bound.

For $x=0$ every $t>0$ is admissible, so $p_U(0)=0$: zero is a lower bound and a proposed positive lower bound $b$ fails at $t=b\mathrm{/}2$. If $U=X$, the same argument gives $p_U(x)=0$ for every $x$.

The gauge is interpreted on the underlying real vector space. No symmetry, balance or positive definiteness is imposed on it by this definition. Convexity uses real coefficients even in the complex case. Neither local convexity of the whole space nor any choice principle is required.