The Distance between Real Matrices

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $m,n\in\mathbb{N}$, with the real matrices $\mathcal{M}_{m\times n}(\mathbb{R})$, their difference $A-B$, and the operator norm $\lVert\cdot\rVert$.

¶ The distance on $\mathcal{M}_{m\times n}(\mathbb{R})$ is the unique map $d$ of The Operator-Norm Distance between Real Matrices Is a Map §map, denoted $d_{m\times n}$, and $d_{n}$ when $m=n$:

$$d_{m\times n}:\mathcal{M}_{m\times n}(\mathbb{R})\times\mathcal{M}_{m\times n}(\mathbb{R})\to\mathbb{R},\qquad d_{m\times n}(A,B)=\lVert A-B\rVert .$$