The Minkowski Gauge of an Open Convex Neighbourhood of the Origin

In the setting of Separable Real Normed Spaces and Hahn–Banach: Notation, let $X$ be a real normed space with zero vector $0_{X}$, and let $U\subseteq X$ be open and convex with $0_{X}\in U$.

(i) Gauge. The gauge of $U$ is the function $p_{U}:X\to\mathbb{R}$ given by

$$p_{U}(x)=\inf\{t\in\mathbb{R}:t>0\text{ and }t^{-1}x\in U\},$$

the infimum existing by The Scaling Set of an Open Convex Neighbourhood of the Origin Has an Infimum (iii).