The Earlier and the New Versions of the Definitions of Symmetric and Positive Semidefinite Matrices, the Operator Norm, Matrix Distance, Eigenvalues and Square Roots Agree

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, with Euclidean space $\mathbb{R}^{n}$, the set $\mathcal{M}_{m\times n}(\mathbb{R})$ of real $m\times n$ matrices and $\mathcal{M}_{n}(\mathbb{R})=\mathcal{M}_{n\times n}(\mathbb{R})$, for $m,n\in\mathbb{N}$.

(i) Symmetric matrices. For every $n\in\mathbb{N}$ and every $A\in\mathcal{M}_{n}(\mathbb{R})$, $A$ is symmetric in the earlier version if and only if it is symmetric in the new version; and the set $\mathcal{S}(n)$ of the earlier version is the set $\mathcal{S}(n)$ of the new version.

(ii) Semidefiniteness. For every $n\in\mathbb{N}$ and every $A\in\mathcal{S}(n)$, $A$ is positive semidefinite in the earlier version if and only if it is positive semidefinite in the new version, and positive definite in the earlier version if and only if it is positive definite in the new version.

(iii) The semidefinite ordering. For every $n\in\mathbb{N}$ and all $X,Y\in\mathcal{S}(n)$, $X\preceq Y$ in the ordering of the earlier version if and only if $X\preceq Y$ in the ordering of the new version.

(iv) Operator norm. For all $m,n\in\mathbb{N}$ and every $A\in\mathcal{M}_{m\times n}(\mathbb{R})$, the operator norm $\lVert A\rVert$ of the earlier version is the operator norm $\lVert A\rVert$ of the new version.

(v) Distance. For all $m,n\in\mathbb{N}$, the distance $d_{m\times n}$ on $\mathcal{M}_{m\times n}(\mathbb{R})$ of the earlier version is the distance $d_{m\times n}$ of the new version.

(vi) Eigenvalues and eigenvectors. For every $n\in\mathbb{N}$, every $A\in\mathcal{M}_{n}(\mathbb{R})$, every $\lambda\in\mathbb{R}$ and every $x\in\mathbb{R}^{n}$, $x$ is an eigenvector of $A$ with eigenvalue $\lambda$ in the earlier version if and only if it is an eigenvector of $A$ with eigenvalue $\lambda$ in the new version; and $\lambda$ is an eigenvalue of $A$ in the earlier version if and only if it is an eigenvalue of $A$ in the new version.

(vii) Square root. For every $n\in\mathbb{N}$ and every positive semidefinite $A\in\mathcal{S}(n)$, the positive semidefinite square root $A^{1/2}$ of the earlier version is the positive semidefinite square root $A^{1/2}$ of the new version.