Table of Contents - 19. COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)

This part contains the definitions and theorems used by the Hilbert Space
Explorer (HSE), mmhil.html. Because it axiomatizes a single complex
Hilbert space whose existence is assumed, its usefulness is limited. For
example, it cannot work with real or quaternion Hilbert spaces and it cannot
study relationships between two Hilbert spaces. More information can be
found on the Hilbert Space Explorer page.

Future development should instead work with general Hilbert spaces as defined
by df-hil; note that df-hil uses extensible structures.

The intent is for this deprecated section to be deleted once all its theorems
have been translated into extensible structure versions (or are not useful).
Many of the theorems in this section have already been translated to
extensible structure versions, but there is still a lot in this section that
might be useful for future reference. It is much easier to translate these
by hand from this section than to start from scratch from textbook proofs,
since the HSE omits no details.