Orthonormal Basis of a Real Inner Product Space

In the setting of Real Hilbert Spaces: Standing Notation and Background, let $E$ be a real inner product space with inner product $\langle\cdot,\cdot\rangle$ and zero vector $0_{E}$, and let $(e_{k})_{k\in\mathbb{N}}$ be an orthonormal sequence in $E$.

¶ The sequence $(e_{k})_{k\in\mathbb{N}}$ is an orthonormal basis of $E$ if the only $x\in E$ satisfying $\langle x,e_{k}\rangle=0$ for every $k\in\mathbb{N}$ is $x=0_{E}$; equivalently, if the orthogonal complement of the set $\{e_{k}:k\in\mathbb{N}\}$ is $\{0_{E}\}$.

An orthonormal basis in this sense is indexed by $\mathbb{N}$ and is therefore an infinite family; a finite-dimensional space is instead described by an orthonormal tuple spanning it, as in Gram-Schmidt Orthonormalisation in a Real Inner Product Space §basis.