Preamble
===

Since we will be dealing with vector spaces of any dimension that are nice to work with when equipped with additional structures like topologies, metrics, norms, and inner products, we can settle with Banach spaces and Hilbert spaces over $\mathbb{R}$ or $\mathbb{C}$. Of course, many results can be generalized to Frechet spaces, locally convex topological vector spaces, or just topological vector spaces. Even the underlying fields can often be relaxed to accomodate non-Archimedean fields. However, we don't attempt to do so, as the current setting very much fits our needs and doesn't introduce unwanted technical details.

The use of the axiom of choice and/or weaker versions that are independent of ZF set theory is indespensible for proving certain important results. Fellow constructivists. Please forgive us.