Orthonormal Basis of a Real Hilbert Space

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

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

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 (ii).