Metamath Proof Explorer

Table of Contents - 18. COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)

The intent is for this deprecated section to be deleted once its theorems have extensible structure versions (or are not useful). You can make a list of "terminal" theorems (i.e., theorems not referenced by anything else) and for each theorem see if there exists an extensible structure version (or decide it is not useful), and if so, delete it. Then, repeat this recursively. One way to search for terminal theorems is to log the output ("MM> OPEN LOG xxx.txt") of "MM> SHOW USAGE " in the Metamath program and search for "(None)".

1. Additional material on group theory (deprecated)
   1. Definitions and basic properties for groups
   2. Abelian groups
2. Complex vector spaces
   1. Definition and basic properties
   2. Examples of complex vector spaces
3. Normed complex vector spaces
   1. Definition and basic properties
   2. Examples of normed complex vector spaces
   3. Induced metric of a normed complex vector space
   4. Inner product
   5. Subspaces
4. Operators on complex vector spaces
   1. Definitions and basic properties
5. Inner product (pre-Hilbert) spaces
   1. Definition and basic properties
   2. Examples of pre-Hilbert spaces
   3. Properties of pre-Hilbert spaces
6. Complex Banach spaces
   1. Definition and basic properties
   2. Examples of complex Banach spaces
   3. Uniform Boundedness Theorem
   4. Minimizing Vector Theorem
7. Complex Hilbert spaces
   1. Definition and basic properties
   2. Standard axioms for a complex Hilbert space
   3. Examples of complex Hilbert spaces
   4. Hellinger-Toeplitz Theorem
8. Appendix: Typesetting definitions for the tokens in this file