The Set of Lengths ‖Ax‖ over the Unit Ball Has a Supremum, and the Supremum Map Exists

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $m,n\in\mathbb{N}$ and let $A\in\mathcal{M}_{m\times n}(\mathbb{R})$ be a real $m\times n$ matrix, with the matrix-vector product $Ax$ of $A$ and a point $x$ of $\mathbb{R}^{n}$, the Euclidean norm $\lVert\cdot\rVert$ on $\mathbb{R}^{n}$ and on $\mathbb{R}^{m}$, and bounded above subsets and suprema of subsets of $\mathbb{R}$ for its order $\le$. Let $U_{n}=\{x\in\mathbb{R}^{n}:\lVert x\rVert\le1\}$ be the closed unit ball of $\mathbb{R}^{n}$. For every $B\in\mathcal{M}_{m\times n}(\mathbb{R})$, let

$$N_{B}=\{\lVert Bx\rVert:x\in U_{n}\}$$

be the image of $U_{n}$ under $x\mapsto\lVert Bx\rVert$, that is, the set of the values $\lVert Bx\rVert$ at the points $x\in U_{n}$ (Images of Typed Terms: the Set of Values $\{t:u\in D\}$ Is a Set, Finite when $D$ Is Finite, and a Typed Term §members). In particular $N_{A}=\{\lVert Ax\rVert:x\in U_{n}\}$.

¶ For every set $s$: $s\in N_{A}$ if and only if $s=\lVert Ax\rVert$ for some $x\in\mathbb{R}^{n}$ with $\lVert x\rVert\le1$. For every set $x$: $x\in U_{n}$ if and only if $x\in\mathbb{R}^{n}$ and $\lVert x\rVert\le1$.

¶ $N_{A}$ is a nonempty subset of $\mathbb{R}$, and $N_{A}$ is bounded above.

¶ $N_{A}$ has a supremum in $\mathbb{R}$.

¶ There is exactly one map $\nu:\mathcal{M}_{m\times n}(\mathbb{R})\to\mathbb{R}$ with $\nu(B)=\sup N_{B}$ for every $B\in\mathcal{M}_{m\times n}(\mathbb{R})$.